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

Metamath Proof Explorer

Theorem pp0ex

Description: The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 24-Jun-1993)

Ref Expression
Assertion pp0ex ⊢ ∅ ∅ ∈ V

Proof

Step Hyp Ref Expression
1 pwpw0 ⊢ 𝒫 ∅ = ∅ ∅
2 p0ex ⊢ ∅ ∈ V
3 2 pwex ⊢ 𝒫 ∅ ∈ V
4 1 3 eqeltrri ⊢ ∅ ∅ ∈ V