Home
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
cA
cB
Assertion
Ref
Expression
ciin
See definition
df-iin
1997
for more information.
Colors of variables:
wff
set
class
metamath.org