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

Metamath Proof Explorer

Theorem 0nep0

Description: The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993)

Ref Expression
Assertion 0nep0 ∅ ≠ { ∅ }

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 1 snnz ⊢ { ∅ } ≠ ∅
3 2 necomi ⊢ ∅ ≠ { ∅ }