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	⊢ 𝒫 𝒫 𝐴 = { 𝑥 ∣ ∪ 𝑥 ⊆ 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		elpwpw	⊢ ( 𝑥 ∈ 𝒫 𝒫 𝐴 ↔ ( 𝑥 ∈ V ∧ ∪ 𝑥 ⊆ 𝐴 ) )
3	1 2	mpbiran	⊢ ( 𝑥 ∈ 𝒫 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴 )
4	3	abbi2i	⊢ 𝒫 𝒫 𝐴 = { 𝑥 ∣ ∪ 𝑥 ⊆ 𝐴 }