Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2on0 Structured version   Visualization version   GIF version

Theorem 2on0 8100
 Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
Assertion
Ref Expression
2on0 2o ≠ ∅

Proof of Theorem 2on0
StepHypRef Expression
1 df-2o 8090 . 2 2o = suc 1o
2 nsuceq0 6249 . 2 suc 1o ≠ ∅
31, 2eqnetri 3081 1 2o ≠ ∅
 Colors of variables: wff setvar class Syntax hints:   ≠ wne 3011  ∅c0 4265  suc csuc 6171  1oc1o 8082  2oc2o 8083 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-11 2161  ax-12 2178  ax-ext 2794  ax-nul 5186 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-v 3471  df-dif 3911  df-un 3913  df-nul 4266  df-sn 4540  df-suc 6175  df-2o 8090 This theorem is referenced by:  snnen2o  8695  pmtrfmvdn0  18581  pmtrsn  18638  efgrcl  18832  goaln0  32714  goalr  32718  fmla0disjsuc  32719  sltval2  33237  sltintdifex  33242  onint1  33871  1oequni2o  34746  finxpreclem4  34772  finxp3o  34778  frlmpwfi  39972  clsk1indlem1  40681
 Copyright terms: Public domain W3C validator