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

Theorem 1onn 6918
Description: One is a natural number. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
1onn  |-  1o  e.  om

Proof of Theorem 1onn
StepHypRef Expression
1 df-1o 6760 . 2  |-  1o  =  suc  (/)
2 peano1 4899 . . 3  |-  (/)  e.  om
3 peano2 4900 . . 3  |-  ( (/)  e.  om  ->  suc  (/)  e.  om )
42, 3ax-mp 5 . 2  |-  suc  (/)  e.  om
51, 4eqeltri 2513 1  |-  1o  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1728   (/)c0 3616   suc csuc 4618   omcom 4880   1oc1o 6753
This theorem is referenced by:  2onn  6919  oaabs2  6924  omabs  6926  nnm2  6928  nnneo  6930  nneob  6931  snfi  7223  1sdom2  7343  1sdom  7347  unxpdom2  7353  en1eqsn  7374  en2  7380  pwfi  7438  wofib  7550  oancom  7642  cnfcom3clem  7698  card1  7893  pm54.43lem  7924  infxpenlem  7933  infxpenc2lem1  7938  infmap2  8136  sdom2en01  8220  cfpwsdom  8497  canthp1lem2  8566  gchcda1  8569  pwxpndom2  8578  pwcdandom  8580  1pi  8798  1lt2pi  8820  indpi  8822  hash2  11712  hash1snb  11719  setcepi  14281  lt6abl  15542  isnzr2  16372  vr1cl  16649  ply1coe  16722  frgpcyg  16892  isppw  20935  en2eleq  27470  en2other2  27471  f1otrspeq  27479  pmtrf  27486  pmtrmvd  27487  pmtrfinv  27491  euhash1  28288  bnj906  29475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pr 4438  ax-un 4736
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-tr 4334  df-eprel 4529  df-po 4538  df-so 4539  df-fr 4576  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-1o 6760
  Copyright terms: Public domain W3C validator