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 A = z | B z
Assertion superuncl x A y A x y A

Proof

Step Hyp Ref Expression
1 superficl.a A = z | B z
2 vex x V
3 vex y V
4 2 3 unex x y V
5 sseq2 z = x y B z B x y
6 sseq2 z = x B z B x
7 sseq2 z = y B z B y
8 ssun3 B x B x y
9 8 adantr B x B y B x y
10 1 4 5 6 7 9 cllem0 x A y A x y A