Theorem 1n0 8544

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 8529	. 2 ⊢ 1o = {∅}
2		0ex 5325	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4801	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3017	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2946  ∅c0 4352  {csn 4648  1_oc1o 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-suc 6401  df-1o 8522

This theorem is referenced by:  nlim1  8545  xp01disj  8547  xp01disjl  8548  enpr2d  9115  map2xp  9213  snnen2o  9300  0sdom1dom  9301  sdom1  9305  sdom1OLD  9306  rex2dom  9309  1sdom2dom  9310  1sdomOLD  9312  unxpdom2  9317  sucxpdom  9318  ssttrcl  9784  ttrclselem2  9795  djuin  9987  eldju2ndl  9993  updjudhcoinrg  10002  card1  10037  pm54.43lem  10069  cflim2  10332  isfin4p1  10384  dcomex  10516  pwcfsdom  10652  cfpwsdom  10653  canthp1lem2  10722  wunex2  10807  1pi  10952  fnpr2o  17617  fnpr2ob  17618  fvpr0o  17619  fvpr1o  17620  fvprif  17621  xpsfrnel  17622  setcepi  18155  setc2obas  18161  frgpuptinv  19813  frgpup3lem  19819  frgpnabllem1  19915  dmdprdpr  20093  dprdpr  20094  coe1mul2lem1  22291  2ndcdisj  23485  xpstopnlem1  23838  sltval2  27719  nosgnn0  27721  sltintdifex  27724  sltres  27725  nogesgn1ores  27737  sltsolem1  27738  nosepnelem  27742  nogt01o  27759  noinfbnd1lem3  27788  noinfbnd2lem1  27793  bnj906  34906  gonan0  35360  gonar  35363  fmla0disjsuc  35366  rankeq1o  36135  onint1  36415  bj-disjsn01  36918  bj-0nel1  36919  bj-1nel0  36920  bj-pr21val  36979  bj-pr22val  36985  finxp1o  37358  finxp2o  37365  domalom  37370  wepwsolem  42999  onov0suclim  43236  clsk3nimkb  44002  clsk1indlem4  44006  clsk1indlem1  44007  prsthinc  48721  prstchom  48744  prstchom2ALT  48746