Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The intersection of two classes
in31
Next ⟩
inrot
Metamath Proof Explorer
Ascii
Unicode
Theorem
in31
Description:
A rearrangement of intersection.
(Contributed by
NM
, 27-Aug-2012)
Ref
Expression
Assertion
in31
⊢
A
∩
B
∩
C
=
C
∩
B
∩
A
Proof
Step
Hyp
Ref
Expression
1
in12
⊢
C
∩
A
∩
B
=
A
∩
C
∩
B
2
incom
⊢
A
∩
B
∩
C
=
C
∩
A
∩
B
3
incom
⊢
C
∩
B
∩
A
=
A
∩
C
∩
B
4
1
2
3
3eqtr4i
⊢
A
∩
B
∩
C
=
C
∩
B
∩
A