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

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

Proof of Theorem 1n0
StepHypRef Expression
1 df1o2 7524 . 2 1𝑜 = {∅}
2 0ex 4755 . . 3 ∅ ∈ V
32snnz 4284 . 2 {∅} ≠ ∅
41, 3eqnetri 2860 1 1𝑜 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2790  c0 3896  {csn 4153  1𝑜c1o 7505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4754
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3191  df-dif 3562  df-un 3564  df-nul 3897  df-sn 4154  df-suc 5693  df-1o 7512
This theorem is referenced by:  xp01disj  7528  map2xp  8082  sdom1  8112  1sdom  8115  unxpdom2  8120  sucxpdom  8121  card1  8746  pm54.43lem  8777  cflim2  9037  isfin4-3  9089  dcomex  9221  pwcfsdom  9357  cfpwsdom  9358  canthp1lem2  9427  wunex2  9512  1pi  9657  xpscfn  16151  xpsc0  16152  xpsc1  16153  xpscfv  16154  xpsfrnel  16155  xpsfrnel2  16157  setcepi  16670  frgpuptinv  18116  frgpup3lem  18122  frgpnabllem1  18208  dmdprdpr  18380  dprdpr  18381  coe1mul2lem1  19569  2ndcdisj  21182  xpstopnlem1  21535  bnj906  30743  sltval2  31545  nosgnn0  31547  sltintdifex  31552  sltres  31553  sltsolem1  31563  nosepnelem  31600  rankeq1o  31955  onint1  32125  bj-disjsn01  32619  bj-0nel1  32622  bj-1nel0  32623  bj-pr21val  32683  bj-pr22val  32689  finxp1o  32896  finxp2o  32903  wepwsolem  37127  clsk3nimkb  37855  clsk1indlem4  37859  clsk1indlem1  37860
  Copyright terms: Public domain W3C validator