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

Theorem 1n0 8110
Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
Assertion
Ref Expression
1n0 1o ≠ ∅

Proof of Theorem 1n0
StepHypRef Expression
1 df1o2 8107 . 2 1o = {∅}
2 0ex 5203 . . 3 ∅ ∈ V
32snnz 4705 . 2 {∅} ≠ ∅
41, 3eqnetri 3086 1 1o ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 3016  c0 4290  {csn 4559  1oc1o 8086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-nul 5202
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3497  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4560  df-suc 6191  df-1o 8093
This theorem is referenced by:  xp01disj  8111  xp01disjl  8112  map2xp  8676  sdom1  8707  1sdom  8710  unxpdom2  8715  sucxpdom  8716  djuin  9336  eldju2ndl  9342  updjudhcoinrg  9351  card1  9386  pm54.43lem  9417  cflim2  9674  isfin4p1  9726  dcomex  9858  pwcfsdom  9994  cfpwsdom  9995  canthp1lem2  10064  wunex2  10149  1pi  10294  fnpr2o  16820  fnpr2ob  16821  fvpr0o  16822  fvpr1o  16823  fvprif  16824  xpsfrnel  16825  setcepi  17338  frgpuptinv  18828  frgpup3lem  18834  frgpnabllem1  18924  dmdprdpr  19102  dprdpr  19103  coe1mul2lem1  20365  2ndcdisj  21994  xpstopnlem1  22347  bnj906  32102  gonan0  32537  gonar  32540  fmla0disjsuc  32543  sltval2  33061  nosgnn0  33063  sltintdifex  33066  sltres  33067  sltsolem1  33078  nosepnelem  33082  rankeq1o  33530  onint1  33695  bj-disjsn01  34162  bj-0nel1  34163  bj-1nel0  34164  bj-pr21val  34223  bj-pr22val  34229  finxp1o  34556  finxp2o  34563  domalom  34568  wepwsolem  39522  clsk3nimkb  40270  clsk1indlem4  40274  clsk1indlem1  40275
  Copyright terms: Public domain W3C validator