symdifass

Description: Symmetric difference is associative. (Contributed by Scott Fenton, 24-Apr-2012) (Proof shortened by BJ, 7-Sep-2022)

		Ref	Expression
	Assertion	symdifass	$⊢ ((A ∆ B) ∆ C) = (A ∆ (B ∆ C))$

Step	Hyp	Ref	Expression
1		elsymdifxor	$⊢ x \in ((A ∆ B) ∆ C) \leftrightarrow (x \in (A ∆ B) ⊻ x \in C)$
2		elsymdifxor	$⊢ x \in (A ∆ B) \leftrightarrow (x \in A ⊻ x \in B)$
3		biid	$⊢ x \in C \leftrightarrow x \in C$
4	2 3	xorbi12i	$⊢ (x \in (A ∆ B) ⊻ x \in C) \leftrightarrow ((x \in A ⊻ x \in B) ⊻ x \in C)$
5		xorass	$⊢ ((x \in A ⊻ x \in B) ⊻ x \in C) \leftrightarrow (x \in A ⊻ (x \in B ⊻ x \in C))$
6		biid	$⊢ x \in A \leftrightarrow x \in A$
7		elsymdifxor	$⊢ x \in (B ∆ C) \leftrightarrow (x \in B ⊻ x \in C)$
8	7	bicomi	$⊢ (x \in B ⊻ x \in C) \leftrightarrow x \in (B ∆ C)$
9	6 8	xorbi12i	$⊢ (x \in A ⊻ (x \in B ⊻ x \in C)) \leftrightarrow (x \in A ⊻ x \in (B ∆ C))$
10	4 5 9	3bitri	$⊢ (x \in (A ∆ B) ⊻ x \in C) \leftrightarrow (x \in A ⊻ x \in (B ∆ C))$
11		elsymdifxor	$⊢ x \in (A ∆ (B ∆ C)) \leftrightarrow (x \in A ⊻ x \in (B ∆ C))$
12	11	bicomi	$⊢ (x \in A ⊻ x \in (B ∆ C)) \leftrightarrow x \in (A ∆ (B ∆ C))$
13	1 10 12	3bitri	$⊢ x \in ((A ∆ B) ∆ C) \leftrightarrow x \in (A ∆ (B ∆ C))$
14	13	eqriv	$⊢ ((A ∆ B) ∆ C) = (A ∆ (B ∆ C))$

Metamath Proof Explorer