Theorem 1n0 8484

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 8469	. 2 ⊢ 1o = {∅}
2		0ex 5298	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4773	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3003	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2932  ∅c0 4315  {csn 4621  1_oc1o 8455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5297

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-v 3468  df-dif 3944  df-un 3946  df-nul 4316  df-sn 4622  df-suc 6361  df-1o 8462

This theorem is referenced by:  nlim1  8485  xp01disj  8487  xp01disjl  8488  enpr2d  9046  map2xp  9144  snnen2o  9234  0sdom1dom  9235  sdom1  9239  sdom1OLD  9240  rex2dom  9243  1sdom2dom  9244  1sdomOLD  9246  unxpdom2  9251  sucxpdom  9252  ssttrcl  9707  ttrclselem2  9718  djuin  9910  eldju2ndl  9916  updjudhcoinrg  9925  card1  9960  pm54.43lem  9992  cflim2  10255  isfin4p1  10307  dcomex  10439  pwcfsdom  10575  cfpwsdom  10576  canthp1lem2  10645  wunex2  10730  1pi  10875  fnpr2o  17504  fnpr2ob  17505  fvpr0o  17506  fvpr1o  17507  fvprif  17508  xpsfrnel  17509  setcepi  18042  setc2obas  18048  frgpuptinv  19683  frgpup3lem  19689  frgpnabllem1  19785  dmdprdpr  19963  dprdpr  19964  coe1mul2lem1  22110  2ndcdisj  23284  xpstopnlem1  23637  sltval2  27508  nosgnn0  27510  sltintdifex  27513  sltres  27514  nogesgn1ores  27526  sltsolem1  27527  nosepnelem  27531  nogt01o  27548  noinfbnd1lem3  27577  noinfbnd2lem1  27582  bnj906  34432  gonan0  34874  gonar  34877  fmla0disjsuc  34880  rankeq1o  35639  onint1  35825  bj-disjsn01  36324  bj-0nel1  36325  bj-1nel0  36326  bj-pr21val  36385  bj-pr22val  36391  finxp1o  36764  finxp2o  36771  domalom  36776  wepwsolem  42298  onov0suclim  42538  clsk3nimkb  43305  clsk1indlem4  43309  clsk1indlem1  43310  prsthinc  47886  prstchom  47909  prstchom2ALT  47911