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

Theorem 2on0 8429
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 8414 . 2 2o = suc 1o
2 nsuceq0 6401 . 2 suc 1o ≠ ∅
31, 2eqnetri 3015 1 2o ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2944  c0 4283  suc csuc 6320  1oc1o 8406  2oc2o 8407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-nul 5264
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-v 3448  df-dif 3914  df-un 3916  df-nul 4284  df-sn 4588  df-suc 6324  df-2o 8414
This theorem is referenced by:  ord2eln012  8444  snnen2oOLD  9172  snnen2o  9182  1sdom2  9185  1sdom2dom  9192  pmtrfmvdn0  19245  pmtrsn  19302  efgrcl  19498  sltval2  27007  sltintdifex  27012  nogt01o  27047  noinfbnd1lem5  27078  noinfbnd2lem1  27081  goaln0  33990  goalr  33994  fmla0disjsuc  33995  onint1  34924  1oequni2o  35842  finxpreclem4  35868  finxp3o  35874  frlmpwfi  41428  clsk1indlem1  42324
  Copyright terms: Public domain W3C validator