Theorem nnon 7909

Description: A natural number is an ordinal number. (Contributed by NM, 27-Jun-1994.)

Assertion

Ref	Expression
nnon	⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Proof of Theorem nnon

Step	Hyp	Ref	Expression
1		omsson 7907	. 2 ⊢ ω ⊆ On
2	1	sseli 4004	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2108  Oncon0 6395  ωcom 7903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-ss 3993  df-om 7904

This theorem is referenced by:  nnoni  7910  nnord  7911  peano4  7931  findsg  7937  onasuc  8584  onmsuc  8585  nna0  8660  nnm0  8661  nnasuc  8662  nnmsuc  8663  nnesuc  8664  nnecl  8669  nnawordi  8677  nnmword  8689  nnawordex  8693  nnaordex  8694  oaabslem  8703  oaabs  8704  oaabs2  8705  omabslem  8706  omabs  8707  nnneo  8711  nneob  8712  naddoa  8758  omnaddcl  8759  dif1ennn  9227  findcard2  9230  onfin2  9294  nndomo  9296  findcard3  9346  findcard3OLD  9347  dffi3  9500  card2inf  9624  elom3  9717  cantnfp1lem3  9749  cnfcomlem  9768  cnfcom  9769  cnfcom3  9773  ttrcltr  9785  ttrclselem1  9794  ttrclselem2  9795  finnum  10017  cardnn  10032  nnsdomel  10059  harsucnn  10067  nnadjuALT  10268  ficardun2  10271  ackbij1lem15  10302  ackbij2lem2  10308  ackbij2lem3  10309  ackbij2  10311  fin23lem22  10396  isf32lem5  10426  fin1a2lem4  10472  fin1a2lem9  10477  pwfseqlem3  10729  winainflem  10762  wunr1om  10788  tskr1om  10836  grothomex  10898  pion  10948  om2uzlt2i  14002  madefi  27968  oldfi  27969  precsexlem3  28251  precsexlem4  28252  precsexlem5  28253  om2noseqlt  28323  om2noseqlt2  28324  zs12bday  28442  constrfin  33736  bnj168  34706  satfvsuc  35329  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  elhf2  36139  findreccl  36419  rdgeqoa  37336  exrecfnlem  37345  finxpreclem4  37360  finxpreclem6  37362  harinf  42991  onexoegt  43205  oaabsb  43256  nnoeomeqom  43274  cantnfub  43283  dflim5  43291  onmcl  43293  omabs2  43294  tfsconcat0b  43308  naddcnffo  43326  naddonnn  43357  naddwordnexlem0  43358  naddwordnexlem3  43361  oawordex3  43362  naddwordnexlem4  43363  omssrncard  43502  nna1iscard  43507