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

Theorem 1n0 7746
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 7743 . 2 1𝑜 = {∅}
2 0ex 4942 . . 3 ∅ ∈ V
32snnz 4452 . 2 {∅} ≠ ∅
41, 3eqnetri 3002 1 1𝑜 ≠ ∅
Colors of variables: wff setvar class
Syntax hints:  wne 2932  c0 4058  {csn 4321  1𝑜c1o 7723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-v 3342  df-dif 3718  df-un 3720  df-nul 4059  df-sn 4322  df-suc 5890  df-1o 7730
This theorem is referenced by:  xp01disj  7747  map2xp  8297  sdom1  8327  1sdom  8330  unxpdom2  8335  sucxpdom  8336  djuin  8955  eldju2ndl  8960  updjudhcoinrg  8969  card1  9004  pm54.43lem  9035  cflim2  9297  isfin4-3  9349  dcomex  9481  pwcfsdom  9617  cfpwsdom  9618  canthp1lem2  9687  wunex2  9772  1pi  9917  xpscfn  16441  xpsc0  16442  xpsc1  16443  xpscfv  16444  xpsfrnel  16445  xpsfrnel2  16447  setcepi  16959  frgpuptinv  18404  frgpup3lem  18410  frgpnabllem1  18496  dmdprdpr  18668  dprdpr  18669  coe1mul2lem1  19859  2ndcdisj  21481  xpstopnlem1  21834  bnj906  31328  sltval2  32136  nosgnn0  32138  sltintdifex  32141  sltres  32142  sltsolem1  32153  nosepnelem  32157  rankeq1o  32605  onint1  32775  bj-disjsn01  33262  bj-0nel1  33264  bj-1nel0  33265  bj-pr21val  33325  bj-pr22val  33331  finxp1o  33558  finxp2o  33565  wepwsolem  38132  clsk3nimkb  38858  clsk1indlem4  38862  clsk1indlem1  38863
  Copyright terms: Public domain W3C validator