Metamath Proof Explorer

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 = x | x A


Step Hyp Ref Expression
1 vex x V
2 elpwpw x 𝒫 𝒫 A x V x A
3 1 2 mpbiran x 𝒫 𝒫 A x A
4 3 abbi2i 𝒫 𝒫 A = x | x A