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 
 |-  (/) e. _V
2 1 snnz 
 |-  { (/) } =/= (/)
3 2 necomi 
 |-  (/) =/= { (/) }