Theorem sssymdifcl 37877

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

Hypothesis

Ref	Expression
ssficl.a	⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}

Assertion

Ref	Expression
sssymdifcl	⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴

Distinct variable groups:   𝑥,𝑦,𝑧   𝑦,𝐴   𝑧,𝐵

Allowed substitution hints:   𝐴(𝑥,𝑧)   𝐵(𝑥,𝑦)

Proof of Theorem sssymdifcl

Step	Hyp	Ref	Expression
1		ssficl.a	. 2 ⊢ 𝐴 = {𝑧 ∣ 𝑧 ⊆ 𝐵}
2		vex 3203	. . . 4 ⊢ 𝑥 ∈ V
3		difexg 4808	. . . 4 ⊢ (𝑥 ∈ V → (𝑥 ∖ 𝑦) ∈ V)
4	2, 3	ax-mp 5	. . 3 ⊢ (𝑥 ∖ 𝑦) ∈ V
5		vex 3203	. . . 4 ⊢ 𝑦 ∈ V
6		difexg 4808	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∖ 𝑥) ∈ V)
7	5, 6	ax-mp 5	. . 3 ⊢ (𝑦 ∖ 𝑥) ∈ V
8	4, 7	unex 6956	. 2 ⊢ ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ V
9		sseq1 3626	. 2 ⊢ (𝑧 = ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) → (𝑧 ⊆ 𝐵 ↔ ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ⊆ 𝐵))
10		sseq1 3626	. 2 ⊢ (𝑧 = 𝑥 → (𝑧 ⊆ 𝐵 ↔ 𝑥 ⊆ 𝐵))
11		sseq1 3626	. 2 ⊢ (𝑧 = 𝑦 → (𝑧 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵))
12		ssdifss 3741	. . 3 ⊢ (𝑥 ⊆ 𝐵 → (𝑥 ∖ 𝑦) ⊆ 𝐵)
13		ssdifss 3741	. . 3 ⊢ (𝑦 ⊆ 𝐵 → (𝑦 ∖ 𝑥) ⊆ 𝐵)
14		unss 3787	. . . 4 ⊢ (((𝑥 ∖ 𝑦) ⊆ 𝐵 ∧ (𝑦 ∖ 𝑥) ⊆ 𝐵) ↔ ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ⊆ 𝐵)
15	14	biimpi 206	. . 3 ⊢ (((𝑥 ∖ 𝑦) ⊆ 𝐵 ∧ (𝑦 ∖ 𝑥) ⊆ 𝐵) → ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ⊆ 𝐵)
16	12, 13, 15	syl2an 494	. 2 ⊢ ((𝑥 ⊆ 𝐵 ∧ 𝑦 ⊆ 𝐵) → ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ⊆ 𝐵)
17	1, 8, 9, 10, 11, 16	cllem0 37871	1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ∖ 𝑦) ∪ (𝑦 ∖ 𝑥)) ∈ 𝐴

Syntax hints:   ∧ wa 384   = wceq 1483   ∈ wcel 1990  {cab 2608  ∀wral 2912  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437

This theorem is referenced by: (None)