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

Theorem 1onn 6868
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 6710 . 2  |-  1o  =  suc  (/)
2 peano1 4850 . . 3  |-  (/)  e.  om
3 peano2 4851 . . 3  |-  ( (/)  e.  om  ->  suc  (/)  e.  om )
42, 3ax-mp 8 . 2  |-  suc  (/)  e.  om
51, 4eqeltri 2500 1  |-  1o  e.  om
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   (/)c0 3615   suc csuc 4570   omcom 4831   1oc1o 6703
This theorem is referenced by:  2onn  6869  oaabs2  6874  omabs  6876  nnm2  6878  nnneo  6880  nneob  6881  snfi  7173  1sdom2  7293  1sdom  7297  unxpdom2  7303  en1eqsn  7324  en2  7330  pwfi  7388  wofib  7498  oancom  7590  cnfcom3clem  7646  card1  7839  pm54.43lem  7870  infxpenlem  7879  infxpenc2lem1  7884  infmap2  8082  sdom2en01  8166  cfpwsdom  8443  canthp1lem2  8512  gchcda1  8515  pwxpndom2  8524  pwcdandom  8526  1pi  8744  1lt2pi  8766  indpi  8768  hash2  11657  hash1snb  11664  setcepi  14226  lt6abl  15487  isnzr2  16317  vr1cl  16594  ply1coe  16667  frgpcyg  16837  isppw  20880  en2eleq  27291  en2other2  27292  f1otrspeq  27300  pmtrf  27307  pmtrmvd  27308  pmtrfinv  27312  euhash1  28040  bnj906  29053
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-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390  ax-un 4687
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-ral 2697  df-rex 2698  df-rab 2701  df-v 2945  df-sbc 3149  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-pss 3323  df-nul 3616  df-if 3727  df-pw 3788  df-sn 3807  df-pr 3808  df-tp 3809  df-op 3810  df-uni 4003  df-br 4200  df-opab 4254  df-tr 4290  df-eprel 4481  df-po 4490  df-so 4491  df-fr 4528  df-we 4530  df-ord 4571  df-on 4572  df-lim 4573  df-suc 4574  df-om 4832  df-1o 6710
  Copyright terms: Public domain W3C validator