Theorem pwpwab

Description: The double power class written as a class abstraction: the class of sets whose union is included in the given class. (Contributed by BJ, 29-Apr-2021)

	Ref	Expression
Assertion	pwpwab	$$⊢𝒫𝒫A=\left\{x|\bigcup x\subseteq A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		elpwpw	$$⊢x\in 𝒫𝒫A\leftrightarrow \left(x\in \mathrm{V}\wedge \bigcup x\subseteq A\right)$$
3	1 2	mpbiran	$$⊢x\in 𝒫𝒫A\leftrightarrow \bigcup x\subseteq A$$
4	3	eqabi	$$⊢𝒫𝒫A=\left\{x|\bigcup x\subseteq A\right\}$$