Theorem ssuncl

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

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

Proof

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