Metamath Proof Explorer

Theorem symdifeq1

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

		Ref	Expression
	Assertion	symdifeq1	$⊢ A = B \to (A ∆ C) = (B ∆ C)$

Step	Hyp	Ref	Expression
1		difeq1	$⊢ A = B \to A ∖ C = B ∖ C$
2		difeq2	$⊢ A = B \to C ∖ A = C ∖ B$
3	1 2	uneq12d	$⊢ A = B \to (A ∖ C) \cup (C ∖ A) = (B ∖ C) \cup (C ∖ B)$
4		df-symdif	$⊢ (A ∆ C) = (A ∖ C) \cup (C ∖ A)$
5		df-symdif	$⊢ (B ∆ C) = (B ∖ C) \cup (C ∖ B)$
6	3 4 5	3eqtr4g	$⊢ A = B \to (A ∆ C) = (B ∆ C)$