Theorem 1n0 8455

Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)

Assertion

Ref	Expression
1n0	⊢ 1o ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df1o2 8444	. 2 ⊢ 1o = {∅}
2		0ex 5265	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4743	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2996	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2926  ∅c0 4299  {csn 4592  1_oc1o 8430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300  df-sn 4593  df-suc 6341  df-1o 8437

This theorem is referenced by:  nlim1  8456  xp01disj  8458  xp01disjl  8459  enpr2d  9023  map2xp  9117  snnen2o  9191  0sdom1dom  9192  sdom1  9196  sdom1OLD  9197  rex2dom  9200  1sdom2dom  9201  1sdomOLD  9203  unxpdom2  9208  sucxpdom  9209  ssttrcl  9675  ttrclselem2  9686  djuin  9878  eldju2ndl  9884  updjudhcoinrg  9893  card1  9928  pm54.43lem  9960  cflim2  10223  isfin4p1  10275  dcomex  10407  pwcfsdom  10543  cfpwsdom  10544  canthp1lem2  10613  wunex2  10698  1pi  10843  fnpr2o  17527  fnpr2ob  17528  fvpr0o  17529  fvpr1o  17530  fvprif  17531  xpsfrnel  17532  setcepi  18057  setc2obas  18063  frgpuptinv  19708  frgpup3lem  19714  frgpnabllem1  19810  dmdprdpr  19988  dprdpr  19989  coe1mul2lem1  22160  2ndcdisj  23350  xpstopnlem1  23703  sltval2  27575  nosgnn0  27577  sltintdifex  27580  sltres  27581  nogesgn1ores  27593  sltsolem1  27594  nosepnelem  27598  nogt01o  27615  noinfbnd1lem3  27644  noinfbnd2lem1  27649  bnj906  34927  gonan0  35386  gonar  35389  fmla0disjsuc  35392  rankeq1o  36166  onint1  36444  bj-disjsn01  36947  bj-0nel1  36948  bj-1nel0  36949  bj-pr21val  37008  bj-pr22val  37014  finxp1o  37387  finxp2o  37394  domalom  37399  wepwsolem  43038  onov0suclim  43270  clsk3nimkb  44036  clsk1indlem4  44040  clsk1indlem1  44041  nelsubc3  49064  prsthinc  49457  prstchom  49555  prstchom2ALT  49557