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

Metamath Proof Explorer

Theorem 0elpw

Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007)

Ref Expression
Assertion 0elpw ⊢ ∅ ∈ 𝒫 A

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ A
2 0ex ⊢ ∅ ∈ V
3 2 elpw ⊢ ∅ ∈ 𝒫 A ↔ ∅ ⊆ A
4 1 3 mpbir ⊢ ∅ ∈ 𝒫 A