Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
Combinations of difference, union, and intersection of two classes
dif32
Next ⟩
difabs
Metamath Proof Explorer
Ascii
Unicode
Theorem
dif32
Description:
Swap second and third argument of double difference.
(Contributed by
NM
, 18-Aug-2004)
Ref
Expression
Assertion
dif32
⊢
A
∖
B
∖
C
=
A
∖
C
∖
B
Proof
Step
Hyp
Ref
Expression
1
uncom
⊢
B
∪
C
=
C
∪
B
2
1
difeq2i
⊢
A
∖
B
∪
C
=
A
∖
C
∪
B
3
difun1
⊢
A
∖
B
∪
C
=
A
∖
B
∖
C
4
difun1
⊢
A
∖
C
∪
B
=
A
∖
C
∖
B
5
2
3
4
3eqtr3i
⊢
A
∖
B
∖
C
=
A
∖
C
∖
B