Theorem bj-sselpwuni

Description: Quantitative version of ssexg : a subset of an element of a class is an element of the powerclass of the union of that class. (Contributed by BJ, 6-Apr-2024)

	Ref	Expression
Assertion	bj-sselpwuni	|- ( ( A C_ B /\ B e. V ) -> A e. ~P U. V )

Proof

Step	Hyp	Ref	Expression
1		ssexg	|- ( ( A C_ B /\ B e. V ) -> A e. _V )
2		ssuni	|- ( ( A C_ B /\ B e. V ) -> A C_ U. V )
3	1 2	elpwd	|- ( ( A C_ B /\ B e. V ) -> A e. ~P U. V )