Theorem elpwpwel

Description: A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023)

	Ref	Expression
Assertion	elpwpwel	$$⊢A\in 𝒫𝒫B\leftrightarrow \bigcup A\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		uniexb	$$⊢A\in \mathrm{V}\leftrightarrow \bigcup A\in \mathrm{V}$$
2	1	anbi1i	$$⊢\left(A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)\leftrightarrow \left(\bigcup A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$
3		elpwpw	$$⊢A\in 𝒫𝒫B\leftrightarrow \left(A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$
4		elpwb	$$⊢\bigcup A\in 𝒫B\leftrightarrow \left(\bigcup A\in \mathrm{V}\wedge \bigcup A\subseteq B\right)$$
5	2 3 4	3bitr4i	$$⊢A\in 𝒫𝒫B\leftrightarrow \bigcup A\in 𝒫B$$