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	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in 𝒫\bigcup V$$

Proof

Step	Hyp	Ref	Expression
1		ssexg	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in \mathrm{V}$$
2		ssuni	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\subseteq \bigcup V$$
3	1 2	elpwd	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in 𝒫\bigcup V$$