Metamath Proof Explorer


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 B B V A 𝒫 V

Proof

Step Hyp Ref Expression
1 ssexg A B B V A V
2 ssuni A B B V A V
3 1 2 elpwd A B B V A 𝒫 V