HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

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 e. A B

See definition df-iin 1997 for more information.

Colors of variables: wff set class
metamath.org