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

Theorem 1n0 7732
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 7729 . 2 1𝑜 = {∅}
2 0ex 4925 . . 3 ∅ ∈ V
32snnz 4445 . 2 {∅} ≠ ∅
41, 3eqnetri 3013 1 1𝑜 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2943  c0 4063  {csn 4317  1𝑜c1o 7709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-v 3353  df-dif 3726  df-un 3728  df-nul 4064  df-sn 4318  df-suc 5871  df-1o 7716
This theorem is referenced by:  xp01disj  7733  map2xp  8289  sdom1  8319  1sdom  8322  unxpdom2  8327  sucxpdom  8328  djuin  8947  eldju2ndl  8953  updjudhcoinrg  8962  card1  8997  pm54.43lem  9028  cflim2  9290  isfin4-3  9342  dcomex  9474  pwcfsdom  9610  cfpwsdom  9611  canthp1lem2  9680  wunex2  9765  1pi  9910  xpscfn  16426  xpsc0  16427  xpsc1  16428  xpscfv  16429  xpsfrnel  16430  xpsfrnel2  16432  setcepi  16944  frgpuptinv  18390  frgpup3lem  18396  frgpnabllem1  18482  dmdprdpr  18655  dprdpr  18656  coe1mul2lem1  19851  2ndcdisj  21479  xpstopnlem1  21832  bnj906  31337  sltval2  32145  nosgnn0  32147  sltintdifex  32150  sltres  32151  sltsolem1  32162  nosepnelem  32166  rankeq1o  32614  onint1  32784  bj-disjsn01  33268  bj-0nel1  33270  bj-1nel0  33271  bj-pr21val  33331  bj-pr22val  33337  finxp1o  33565  finxp2o  33572  wepwsolem  38138  clsk3nimkb  38864  clsk1indlem4  38868  clsk1indlem1  38869
  Copyright terms: Public domain W3C validator