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