Theorem elpwpw

Description: Characterization of the elements of a double power class: they are exactly the sets whose union is included in that class. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	elpwpw	$$⊢A\in 𝒫𝒫B\leftrightarrow \left(A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwb	$$⊢A\in 𝒫𝒫B\leftrightarrow \left(A\in \mathrm{V}\wedge A\subseteq 𝒫B\right)$$
2		sspwuni	$$⊢A\subseteq 𝒫B\leftrightarrow \bigcup A\subseteq B$$
3	2	anbi2i	$$⊢\left(A\in \mathrm{V}\wedge A\subseteq 𝒫B\right)\leftrightarrow \left(A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$
4	1 3	bitri	$$⊢A\in 𝒫𝒫B\leftrightarrow \left(A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$