MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1n0 Unicode version

Theorem 1n0 6730
Description: Ordinal one is not equal to ordinal zero. (Contributed by NM, 26-Dec-2004.)
Assertion
Ref Expression
1n0  |-  1o  =/=  (/)

Proof of Theorem 1n0
StepHypRef Expression
1 df1o2 6727 . 2  |-  1o  =  { (/) }
2 0ex 4331 . . 3  |-  (/)  e.  _V
32snnz 3914 . 2  |-  { (/) }  =/=  (/)
41, 3eqnetri 2615 1  |-  1o  =/=  (/)
Colors of variables: wff set class
Syntax hints:    =/= wne 2598   (/)c0 3620   {csn 3806   1oc1o 6708
This theorem is referenced by:  xp01disj  6731  map2xp  7268  sdom1  7299  1sdom  7302  unxpdom2  7308  sucxpdom  7309  card1  7844  pm54.43lem  7875  cflim2  8132  isfin4-3  8184  dcomex  8316  pwcfsdom  8447  cfpwsdom  8448  canthp1lem2  8517  wunex2  8602  1pi  8749  xpscfn  13772  xpsc0  13773  xpsc1  13774  xpscfv  13775  xpsfrnel  13776  xpsfrnel2  13778  setcepi  14231  frgpuptinv  15391  frgpup3lem  15397  frgpnabllem1  15472  dmdprdpr  15595  dprdpr  15596  coe1mul2lem1  16648  2ndcdisj  17507  xpstopnlem1  17829  sltval2  25565  nosgnn0  25567  sltintdifex  25572  sltres  25573  sltsolem1  25577  rankeq1o  26060  onint1  26147  wepwsolem  27053  bnj906  29155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-nul 4330
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-un 3317  df-nul 3621  df-sn 3812  df-suc 4579  df-1o 6715
  Copyright terms: Public domain W3C validator