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 ⊢ ∅ ≠ ∅