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=\left\{z|B\subseteq z\right\}$$
Assertion	superuncl	$$⊢\forall x\in A\forall y\in Ax\cup y\in A$$

Proof

Step	Hyp	Ref	Expression
1		superficl.a	$$⊢A=\left\{z|B\subseteq z\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3		vex	$$⊢y\in \mathrm{V}$$
4	2 3	unex	$$⊢x\cup y\in \mathrm{V}$$
5		sseq2	$$⊢z=x\cup y\to \left(B\subseteq z\leftrightarrow B\subseteq x\cup y\right)$$
6		sseq2	$$⊢z=x\to \left(B\subseteq z\leftrightarrow B\subseteq x\right)$$
7		sseq2	$$⊢z=y\to \left(B\subseteq z\leftrightarrow B\subseteq y\right)$$
8		ssun3	$$⊢B\subseteq x\to B\subseteq x\cup y$$
9	8	adantr	$$⊢\left(B\subseteq x\wedge B\subseteq y\right)\to B\subseteq x\cup y$$
10	1 4 5 6 7 9	cllem0	$$⊢\forall x\in A\forall y\in Ax\cup y\in A$$