Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The union of two classes
un12
Next ⟩
un23
Metamath Proof Explorer
Ascii
Unicode
Theorem
un12
Description:
A rearrangement of union.
(Contributed by
NM
, 12-Aug-2004)
Ref
Expression
Assertion
un12
⊢
A
∪
B
∪
C
=
B
∪
A
∪
C
Proof
Step
Hyp
Ref
Expression
1
uncom
⊢
A
∪
B
=
B
∪
A
2
1
uneq1i
⊢
A
∪
B
∪
C
=
B
∪
A
∪
C
3
unass
⊢
A
∪
B
∪
C
=
A
∪
B
∪
C
4
unass
⊢
B
∪
A
∪
C
=
B
∪
A
∪
C
5
2
3
4
3eqtr3i
⊢
A
∪
B
∪
C
=
B
∪
A
∪
C