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

Proof

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