dfsymdif3

Description: Alternate definition of the symmetric difference, given in Example 4.1 of Stoll p. 262 (the original definition corresponds to Stoll p. 13). (Contributed by NM, 17-Aug-2004) (Revised by BJ, 30-Apr-2020)

		Ref	Expression
	Assertion	dfsymdif3	$⊢ (A ∆ B) = (A \cup B) ∖ (A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		difin	$⊢ A ∖ (A \cap B) = A ∖ B$
2		incom	$⊢ A \cap B = B \cap A$
3	2	difeq2i	$⊢ B ∖ (A \cap B) = B ∖ (B \cap A)$
4		difin	$⊢ B ∖ (B \cap A) = B ∖ A$
5	3 4	eqtri	$⊢ B ∖ (A \cap B) = B ∖ A$
6	1 5	uneq12i	$⊢ (A ∖ (A \cap B)) \cup (B ∖ (A \cap B)) = (A ∖ B) \cup (B ∖ A)$
7		difundir	$⊢ (A \cup B) ∖ (A \cap B) = (A ∖ (A \cap B)) \cup (B ∖ (A \cap B))$
8		df-symdif	$⊢ (A ∆ B) = (A ∖ B) \cup (B ∖ A)$
9	6 7 8	3eqtr4ri	$⊢ (A ∆ B) = (A \cup B) ∖ (A \cap B)$

Metamath Proof Explorer

Theorem dfsymdif3

Proof