Metamath Proof Explorer


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