Theorem 1n0 8467

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 8452	. 2 ⊢ 1o = {∅}
2		0ex 5297	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4770	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 3010	1 ⊢ 1o ≠ ∅

Syntax hints:   ≠ wne 2939  ∅c0 4315  {csn 4619  1_oc1o 8438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-nul 5296

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3472  df-dif 3944  df-un 3946  df-nul 4316  df-sn 4620  df-suc 6356  df-1o 8445

This theorem is referenced by:  nlim1  8468  xp01disj  8470  xp01disjl  8471  enpr2d  9029  map2xp  9127  snnen2o  9217  0sdom1dom  9218  sdom1  9222  sdom1OLD  9223  rex2dom  9226  1sdom2dom  9227  1sdomOLD  9229  unxpdom2  9234  sucxpdom  9235  ssttrcl  9689  ttrclselem2  9700  djuin  9892  eldju2ndl  9898  updjudhcoinrg  9907  card1  9942  pm54.43lem  9974  cflim2  10237  isfin4p1  10289  dcomex  10421  pwcfsdom  10557  cfpwsdom  10558  canthp1lem2  10627  wunex2  10712  1pi  10857  fnpr2o  17482  fnpr2ob  17483  fvpr0o  17484  fvpr1o  17485  fvprif  17486  xpsfrnel  17487  setcepi  18017  setc2obas  18023  frgpuptinv  19600  frgpup3lem  19606  frgpnabllem1  19698  dmdprdpr  19875  dprdpr  19876  coe1mul2lem1  21715  2ndcdisj  22884  xpstopnlem1  23237  sltval2  27081  nosgnn0  27083  sltintdifex  27086  sltres  27087  nogesgn1ores  27099  sltsolem1  27100  nosepnelem  27104  nogt01o  27121  noinfbnd1lem3  27150  noinfbnd2lem1  27155  bnj906  33756  gonan0  34198  gonar  34201  fmla0disjsuc  34204  rankeq1o  34957  onint1  35122  bj-disjsn01  35621  bj-0nel1  35622  bj-1nel0  35623  bj-pr21val  35682  bj-pr22val  35688  finxp1o  36061  finxp2o  36068  domalom  36073  wepwsolem  41541  onov0suclim  41781  clsk3nimkb  42548  clsk1indlem4  42552  clsk1indlem1  42553  prsthinc  47308  prstchom  47331  prstchom2ALT  47333