Metamath Proof Explorer


Theorem p0ex

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT . (Contributed by NM, 23-Dec-1993)

Ref Expression
Assertion p0ex { ∅ } ∈ V

Proof

Step Hyp Ref Expression
1 pw0 𝒫 ∅ = { ∅ }
2 0ex ∅ ∈ V
3 2 pwex 𝒫 ∅ ∈ V
4 1 3 eqeltrri { ∅ } ∈ V