Theorem 1n0 8524

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 8511	. 2 ⊢ 1o = {∅}
2		0ex 5312	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4780	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3008	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2937  ∅c0 4338  {csn 4630  1_oc1o 8497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-un 3967  df-nul 4339  df-sn 4631  df-suc 6391  df-1o 8504

This theorem is referenced by:  nlim1  8525  xp01disj  8527  xp01disjl  8528  enpr2d  9087  map2xp  9185  snnen2o  9270  0sdom1dom  9271  sdom1  9275  sdom1OLD  9276  rex2dom  9279  1sdom2dom  9280  1sdomOLD  9282  unxpdom2  9287  sucxpdom  9288  ssttrcl  9752  ttrclselem2  9763  djuin  9955  eldju2ndl  9961  updjudhcoinrg  9970  card1  10005  pm54.43lem  10037  cflim2  10300  isfin4p1  10352  dcomex  10484  pwcfsdom  10620  cfpwsdom  10621  canthp1lem2  10690  wunex2  10775  1pi  10920  fnpr2o  17603  fnpr2ob  17604  fvpr0o  17605  fvpr1o  17606  fvprif  17607  xpsfrnel  17608  setcepi  18141  setc2obas  18147  frgpuptinv  19803  frgpup3lem  19809  frgpnabllem1  19905  dmdprdpr  20083  dprdpr  20084  coe1mul2lem1  22285  2ndcdisj  23479  xpstopnlem1  23832  sltval2  27715  nosgnn0  27717  sltintdifex  27720  sltres  27721  nogesgn1ores  27733  sltsolem1  27734  nosepnelem  27738  nogt01o  27755  noinfbnd1lem3  27784  noinfbnd2lem1  27789  bnj906  34922  gonan0  35376  gonar  35379  fmla0disjsuc  35382  rankeq1o  36152  onint1  36431  bj-disjsn01  36934  bj-0nel1  36935  bj-1nel0  36936  bj-pr21val  36995  bj-pr22val  37001  finxp1o  37374  finxp2o  37381  domalom  37386  wepwsolem  43030  onov0suclim  43263  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  prsthinc  48854  prstchom  48877  prstchom2ALT  48879