Metamath Proof Explorer


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 𝑥𝐴𝑦𝐴 ( 𝑥𝑦 ) ∈ 𝐴