Theorem symdifeq1

Description: Equality theorem for symmetric difference. (Contributed by Scott Fenton, 24-Apr-2012)

	Ref	Expression
Assertion	symdifeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 △ 𝐶 ) = ( 𝐵 △ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		difeq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐶 ) )
2		difeq2	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) )
3	1 2	uneq12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐴 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐴 ) ) = ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) ) )
4		df-symdif	⊢ ( 𝐴 △ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐴 ) )
5		df-symdif	⊢ ( 𝐵 △ 𝐶 ) = ( ( 𝐵 ∖ 𝐶 ) ∪ ( 𝐶 ∖ 𝐵 ) )
6	3 4 5	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐴 △ 𝐶 ) = ( 𝐵 △ 𝐶 ) )