Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The difference of two classes
difeq12
Next ⟩
difeq1i
Metamath Proof Explorer
Ascii
Unicode
Theorem
difeq12
Description:
Equality theorem for class difference.
(Contributed by
FL
, 31-Aug-2009)
Ref
Expression
Assertion
difeq12
⊢
A
=
B
∧
C
=
D
→
A
∖
C
=
B
∖
D
Proof
Step
Hyp
Ref
Expression
1
difeq1
⊢
A
=
B
→
A
∖
C
=
B
∖
C
2
difeq2
⊢
C
=
D
→
B
∖
C
=
B
∖
D
3
1
2
sylan9eq
⊢
A
=
B
∧
C
=
D
→
A
∖
C
=
B
∖
D