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
in12
Next ⟩
in32
Metamath Proof Explorer
Ascii
Unicode
Theorem
in12
Description:
A rearrangement of intersection.
(Contributed by
NM
, 21-Apr-2001)
Ref
Expression
Assertion
in12
⊢
A
∩
B
∩
C
=
B
∩
A
∩
C
Proof
Step
Hyp
Ref
Expression
1
incom
⊢
A
∩
B
=
B
∩
A
2
1
ineq1i
⊢
A
∩
B
∩
C
=
B
∩
A
∩
C
3
inass
⊢
A
∩
B
∩
C
=
A
∩
B
∩
C
4
inass
⊢
B
∩
A
∩
C
=
B
∩
A
∩
C
5
2
3
4
3eqtr3i
⊢
A
∩
B
∩
C
=
B
∩
A
∩
C