This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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