Theorem sssymdifcl

Description: The class of all subsets of a class is closed under symmetric difference. (Contributed by RP, 3-Jan-2020)

	Ref	Expression
Hypothesis	ssficl.a	⊢ 𝐴 = { 𝑧 ∣ 𝑧 ⊆ 𝐵 }
Assertion	sssymdifcl	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	⊢ 𝐴 = { 𝑧 ∣ 𝑧 ⊆ 𝐵 }
2		vex	⊢ 𝑥 ∈ V
3	2	difexi	⊢ ( 𝑥 ∖ 𝑦 ) ∈ V
4		vex	⊢ 𝑦 ∈ V
5	4	difexi	⊢ ( 𝑦 ∖ 𝑥 ) ∈ V
6	3 5	unex	⊢ ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ∈ V
7		sseq1	⊢ ( 𝑧 = ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) → ( 𝑧 ⊆ 𝐵 ↔ ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ⊆ 𝐵 ) )
8		sseq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ⊆ 𝐵 ↔ 𝑥 ⊆ 𝐵 ) )
9		sseq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵 ) )
10		ssdifss	⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ∖ 𝑦 ) ⊆ 𝐵 )
11		ssdifss	⊢ ( 𝑦 ⊆ 𝐵 → ( 𝑦 ∖ 𝑥 ) ⊆ 𝐵 )
12		unss	⊢ ( ( ( 𝑥 ∖ 𝑦 ) ⊆ 𝐵 ∧ ( 𝑦 ∖ 𝑥 ) ⊆ 𝐵 ) ↔ ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ⊆ 𝐵 )
13	12	biimpi	⊢ ( ( ( 𝑥 ∖ 𝑦 ) ⊆ 𝐵 ∧ ( 𝑦 ∖ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ⊆ 𝐵 )
14	10 11 13	syl2an	⊢ ( ( 𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵 ) → ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ⊆ 𝐵 )
15	1 6 7 8 9 14	cllem0	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝑥 ∖ 𝑦 ) ∪ ( 𝑦 ∖ 𝑥 ) ) ∈ 𝐴