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 = { z | z C_ B }
Assertion	ssuncl	|- A. x e. A A. y e. A ( x u. y ) e. A

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	|- A = { z | z C_ B }
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	unex	|- ( x u. y ) e. _V
5		sseq1	|- ( z = ( x u. y ) -> ( z C_ B <-> ( x u. y ) C_ B ) )
6		sseq1	|- ( z = x -> ( z C_ B <-> x C_ B ) )
7		sseq1	|- ( z = y -> ( z C_ B <-> y C_ B ) )
8		unss	|- ( ( x C_ B /\ y C_ B ) <-> ( x u. y ) C_ B )
9	8	biimpi	|- ( ( x C_ B /\ y C_ B ) -> ( x u. y ) C_ B )
10	1 4 5 6 7 9	cllem0	|- A. x e. A A. y e. A ( x u. y ) e. A