Metamath Proof Explorer


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