Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The difference, union, and intersection of two classes
The symmetric difference of two classes
symdifeq2
Next ⟩
nfsymdif
Metamath Proof Explorer
Ascii
Unicode
Theorem
symdifeq2
Description:
Equality theorem for symmetric difference.
(Contributed by
Scott Fenton
, 24-Apr-2012)
Ref
Expression
Assertion
symdifeq2
⊢
A
=
B
→
C
∆
A
=
C
∆
B
Proof
Step
Hyp
Ref
Expression
1
symdifeq1
⊢
A
=
B
→
A
∆
C
=
B
∆
C
2
symdifcom
⊢
C
∆
A
=
A
∆
C
3
symdifcom
⊢
C
∆
B
=
B
∆
C
4
1
2
3
3eqtr4g
⊢
A
=
B
→
C
∆
A
=
C
∆
B