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

Theorem 2on0 8522
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 8507 . 2 2o = suc 1o
2 nsuceq0 6467 . 2 suc 1o ≠ ∅
31, 2eqnetri 3011 1 2o ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2940  c0 4333  suc csuc 6386  1oc1o 8499  2oc2o 8500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-nul 4334  df-sn 4627  df-suc 6390  df-2o 8507
This theorem is referenced by:  ord2eln012  8535  snnen2oOLD  9264  snnen2o  9273  1sdom2  9276  1sdom2dom  9283  pmtrfmvdn0  19480  pmtrsn  19537  efgrcl  19733  sltval2  27701  sltintdifex  27706  nogt01o  27741  noinfbnd1lem5  27772  noinfbnd2lem1  27775  goaln0  35398  goalr  35402  fmla0disjsuc  35403  onint1  36450  1oequni2o  37369  finxpreclem4  37395  finxp3o  37401  frlmpwfi  43110  clsk1indlem1  44058
  Copyright terms: Public domain W3C validator