Theorem nnon 7812

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

Syntax hints:   → wi 4   ∈ wcel 2119  Oncon0 6310  ωcom 7806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-ss 3900  df-om 7807

This theorem is referenced by:  nnoni  7813  nnord  7814  peano4  7832  findsg  7837  onasuc  8453  onmsuc  8454  nna0  8530  nnm0  8531  nnasuc  8532  nnmsuc  8533  nnesuc  8534  nnecl  8539  nnawordi  8547  nnmword  8559  nnawordex  8563  nnaordex  8564  oaabslem  8573  oaabs  8574  oaabs2  8575  omabslem  8576  omabs  8577  nnneo  8581  nneob  8582  naddoa  8628  omnaddcl  8629  dif1ennn  9087  findcard2  9089  onfin2  9141  nndomo  9142  findcard3  9183  dffi3  9334  card2inf  9460  elom3  9560  cantnfp1lem3  9592  cnfcomlem  9611  cnfcom  9612  cnfcom3  9616  ttrcltr  9628  ttrclselem1  9637  ttrclselem2  9638  finnum  9863  cardnn  9878  nnsdomel  9905  harsucnn  9913  nnadjuALT  10112  ficardun2  10115  ackbij1lem15  10146  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  fin23lem22  10240  isf32lem5  10270  fin1a2lem4  10316  fin1a2lem9  10321  pwfseqlem3  10574  winainflem  10607  wunr1om  10633  tskr1om  10681  grothomex  10743  pion  10793  om2uzlt2i  13904  madefi  27923  oldfi  27924  precsexlem3  28219  precsexlem4  28220  precsexlem5  28221  om2noseqlt  28309  om2noseqlt2  28310  constrfin  33930  constrextdg2lem  33932  constrext2chnlem  33934  constrfiss  33935  constrllcllem  33936  constrlccllem  33937  constrcccllem  33938  constrcn  33944  constrcjcl  33952  bnj168  34913  fineqvnttrclselem1  35302  fineqvnttrclselem2  35303  fineqvnttrclse  35305  satfvsuc  35589  satf0suc  35604  sat1el2xp  35607  fmlasuc0  35612  elhf2  36403  findreccl  36681  ttctr  36721  ttcmin  36724  dfttc2g  36734  rdgeqoa  37732  exrecfnlem  37741  finxpreclem4  37756  finxpreclem6  37758  harinf  43479  onexoegt  43689  oaabsb  43739  nnoeomeqom  43757  cantnfub  43766  dflim5  43774  onmcl  43776  omabs2  43777  tfsconcat0b  43791  naddcnffo  43809  naddonnn  43840  naddwordnexlem0  43841  naddwordnexlem3  43844  oawordex3  43845  naddwordnexlem4  43846  omssrncard  43984  nna1iscard  43989