Theorem superuncl

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

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

Proof

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