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

Proof

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