Theorem 1n0 7462

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

Assertion

Ref	Expression
1n0	⊢ 1𝑜 ≠ ∅

Proof of Theorem 1n0

Step	Hyp	Ref	Expression
1		df1o2 7459	. 2 ⊢ 1𝑜 = {∅}
2		0ex 4718	. . 3 ⊢ ∅ ∈ V
3	2	snnz 4252	. 2 ⊢ {∅} ≠ ∅
4	1, 3	eqnetri 2852	1 ⊢ 1𝑜 ≠ ∅

Syntax hints:   ≠ wne 2780  ∅c0 3874  {csn 4125  1_𝑜c1o 7440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875  df-sn 4126  df-suc 5646  df-1o 7447

This theorem is referenced by:  xp01disj  7463  map2xp  8015  sdom1  8045  1sdom  8048  unxpdom2  8053  sucxpdom  8054  card1  8677  pm54.43lem  8708  cflim2  8968  isfin4-3  9020  dcomex  9152  pwcfsdom  9284  cfpwsdom  9285  canthp1lem2  9354  wunex2  9439  1pi  9584  xpscfn  16042  xpsc0  16043  xpsc1  16044  xpscfv  16045  xpsfrnel  16046  xpsfrnel2  16048  setcepi  16561  frgpuptinv  18007  frgpup3lem  18013  frgpnabllem1  18099  dmdprdpr  18271  dprdpr  18272  coe1mul2lem1  19458  2ndcdisj  21069  xpstopnlem1  21422  bnj906  30254  sltval2  31053  nosgnn0  31055  sltintdifex  31060  sltres  31061  sltsolem1  31067  rankeq1o  31448  onint1  31618  bj-disjsn01  32130  bj-0nel1  32133  bj-1nel0  32134  bj-pr21val  32194  bj-pr22val  32200  finxp1o  32405  finxp2o  32412  wepwsolem  36630  clsk3nimkb  37358  clsk1indlem4  37362  clsk1indlem1  37363