Metamath Proof Explorer

Theorem 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

Proof

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