Theorem nnon 7893

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 7891	. 2 ⊢ ω ⊆ On
2	1	sseli 3991	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2106  Oncon0 6386  ωcom 7887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-ss 3980  df-om 7888

This theorem is referenced by:  nnoni  7894  nnord  7895  peano4  7915  findsg  7920  onasuc  8565  onmsuc  8566  nna0  8641  nnm0  8642  nnasuc  8643  nnmsuc  8644  nnesuc  8645  nnecl  8650  nnawordi  8658  nnmword  8670  nnawordex  8674  nnaordex  8675  oaabslem  8684  oaabs  8685  oaabs2  8686  omabslem  8687  omabs  8688  nnneo  8692  nneob  8693  naddoa  8739  omnaddcl  8740  dif1ennn  9200  findcard2  9203  onfin2  9266  nndomo  9267  findcard3  9316  findcard3OLD  9317  dffi3  9469  card2inf  9593  elom3  9686  cantnfp1lem3  9718  cnfcomlem  9737  cnfcom  9738  cnfcom3  9742  ttrcltr  9754  ttrclselem1  9763  ttrclselem2  9764  finnum  9986  cardnn  10001  nnsdomel  10028  harsucnn  10036  nnadjuALT  10237  ficardun2  10240  ackbij1lem15  10271  ackbij2lem2  10277  ackbij2lem3  10278  ackbij2  10280  fin23lem22  10365  isf32lem5  10395  fin1a2lem4  10441  fin1a2lem9  10446  pwfseqlem3  10698  winainflem  10731  wunr1om  10757  tskr1om  10805  grothomex  10867  pion  10917  om2uzlt2i  13989  madefi  27965  oldfi  27966  precsexlem3  28248  precsexlem4  28249  precsexlem5  28250  om2noseqlt  28320  om2noseqlt2  28321  zs12bday  28439  constrfin  33751  bnj168  34723  satfvsuc  35346  satf0suc  35361  sat1el2xp  35364  fmlasuc0  35369  elhf2  36157  findreccl  36436  rdgeqoa  37353  exrecfnlem  37362  finxpreclem4  37377  finxpreclem6  37379  harinf  43023  onexoegt  43233  oaabsb  43284  nnoeomeqom  43302  cantnfub  43311  dflim5  43319  onmcl  43321  omabs2  43322  tfsconcat0b  43336  naddcnffo  43354  naddonnn  43385  naddwordnexlem0  43386  naddwordnexlem3  43389  oawordex3  43390  naddwordnexlem4  43391  omssrncard  43530  nna1iscard  43535