Metamath Proof Explorer

Theorem 1n0

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004)

Ref Expression
Assertion 1n0 
|- 1o =/= (/)

Proof

Step Hyp Ref Expression
1 df1o2 
 |-  1o = { (/) }
2 0ex 
 |-  (/) e. _V
3 2 snnz 
 |-  { (/) } =/= (/)
4 1 3 eqnetri 
 |-  1o =/= (/)