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

Theorem 1n0 7194
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 7191 . 2  |-  1o  =  { (/) }
2 0ex 4534 . . 3  |-  (/)  e.  _V
32snnz 4089 . 2  |-  { (/) }  =/=  (/)
41, 3eqnetri 2693 1  |-  1o  =/=  (/)
Colors of variables: wff setvar class
Syntax hints:    =/= wne 2621   (/)c0 3730   {csn 3967   1oc1o 7172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-nul 4533
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-nul 3731  df-sn 3968  df-suc 5428  df-1o 7179
This theorem is referenced by:  xp01disj  7195  map2xp  7739  sdom1  7769  1sdom  7772  unxpdom2  7777  sucxpdom  7778  card1  8399  pm54.43lem  8430  cflim2  8690  isfin4-3  8742  dcomex  8874  pwcfsdom  9005  cfpwsdom  9006  canthp1lem2  9075  wunex2  9160  1pi  9305  xpscfn  15458  xpsc0  15459  xpsc1  15460  xpscfv  15461  xpsfrnel  15462  xpsfrnel2  15464  setcepi  15976  frgpuptinv  17414  frgpup3lem  17420  frgpnabllem1  17502  dmdprdpr  17675  dprdpr  17676  coe1mul2lem1  18853  2ndcdisj  20464  xpstopnlem1  20817  bnj906  29734  sltval2  30536  nosgnn0  30538  sltintdifex  30543  sltres  30544  sltsolem1  30550  rankeq1o  30931  onint1  31102  bj-disjsn01  31536  bj-0nel1  31539  bj-1nel0  31540  bj-pr21val  31600  bj-pr22val  31606  finxp1o  31777  finxp2o  31784  wepwsolem  35894
  Copyright terms: Public domain W3C validator