Syntax Definition ciin 1995

Description: Extend class notation to include indexed intersection.

Hypotheses

Ref	Expression
vx	set x
cA	class A
cB	class B

Assertion

Ref	Expression
ciin	class ∩x ∈ A B

See definition df-iin 1997 for more information.

metamath.org