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

Theorem 1n0 7970
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 7967 . 2 1o = {∅}
2 0ex 5102 . . 3 ∅ ∈ V
32snnz 4618 . 2 {∅} ≠ ∅
41, 3eqnetri 3054 1 1o ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2984  c0 4211  {csn 4472  1oc1o 7946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-nul 5101
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-v 3439  df-dif 3862  df-un 3864  df-nul 4212  df-sn 4473  df-suc 6072  df-1o 7953
This theorem is referenced by:  xp01disj  7971  xp01disjl  7972  map2xp  8534  sdom1  8564  1sdom  8567  unxpdom2  8572  sucxpdom  8573  djuin  9193  eldju2ndl  9199  updjudhcoinrg  9208  card1  9243  pm54.43lem  9274  cflim2  9531  isfin4p1  9583  dcomex  9715  pwcfsdom  9851  cfpwsdom  9852  canthp1lem2  9921  wunex2  10006  1pi  10151  fnpr2o  16659  fnpr2ob  16660  fvpr0o  16661  fvpr1o  16662  fvprif  16663  xpsfrnel  16664  setcepi  17177  frgpuptinv  18624  frgpup3lem  18630  frgpnabllem1  18716  dmdprdpr  18888  dprdpr  18889  coe1mul2lem1  20118  2ndcdisj  21748  xpstopnlem1  22101  bnj906  31818  gonan0  32248  gonar  32251  fmla0disjsuc  32254  sltval2  32773  nosgnn0  32775  sltintdifex  32778  sltres  32779  sltsolem1  32790  nosepnelem  32794  rankeq1o  33242  onint1  33407  bj-disjsn01  33839  bj-0nel1  33840  bj-1nel0  33841  bj-pr21val  33949  bj-pr22val  33955  finxp1o  34223  finxp2o  34230  domalom  34235  wepwsolem  39146  clsk3nimkb  39894  clsk1indlem4  39898  clsk1indlem1  39899
  Copyright terms: Public domain W3C validator