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 e. ( ( A /_\ B ) /_\ C ) <-> ( x e. ( A /_\ B ) \/_ x e. C ) )
2		elsymdifxor	|- ( x e. ( A /_\ B ) <-> ( x e. A \/_ x e. B ) )
3		biid	|- ( x e. C <-> x e. C )
4	2 3	xorbi12i	|- ( ( x e. ( A /_\ B ) \/_ x e. C ) <-> ( ( x e. A \/_ x e. B ) \/_ x e. C ) )
5		xorass	|- ( ( ( x e. A \/_ x e. B ) \/_ x e. C ) <-> ( x e. A \/_ ( x e. B \/_ x e. C ) ) )
6		biid	|- ( x e. A <-> x e. A )
7		elsymdifxor	|- ( x e. ( B /_\ C ) <-> ( x e. B \/_ x e. C ) )
8	7	bicomi	|- ( ( x e. B \/_ x e. C ) <-> x e. ( B /_\ C ) )
9	6 8	xorbi12i	|- ( ( x e. A \/_ ( x e. B \/_ x e. C ) ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
10	4 5 9	3bitri	|- ( ( x e. ( A /_\ B ) \/_ x e. C ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
11		elsymdifxor	|- ( x e. ( A /_\ ( B /_\ C ) ) <-> ( x e. A \/_ x e. ( B /_\ C ) ) )
12	11	bicomi	|- ( ( x e. A \/_ x e. ( B /_\ C ) ) <-> x e. ( A /_\ ( B /_\ C ) ) )
13	1 10 12	3bitri	|- ( x e. ( ( A /_\ B ) /_\ C ) <-> x e. ( A /_\ ( B /_\ C ) ) )
14	13	eqriv	|- ( ( A /_\ B ) /_\ C ) = ( A /_\ ( B /_\ C ) )