Theorem nnon 7848

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

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6332  ωcom 7842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-ss 3931  df-om 7843

This theorem is referenced by:  nnoni  7849  nnord  7850  peano4  7868  findsg  7873  onasuc  8492  onmsuc  8493  nna0  8568  nnm0  8569  nnasuc  8570  nnmsuc  8571  nnesuc  8572  nnecl  8577  nnawordi  8585  nnmword  8597  nnawordex  8601  nnaordex  8602  oaabslem  8611  oaabs  8612  oaabs2  8613  omabslem  8614  omabs  8615  nnneo  8619  nneob  8620  naddoa  8666  omnaddcl  8667  dif1ennn  9125  findcard2  9128  onfin2  9180  nndomo  9181  findcard3  9229  findcard3OLD  9230  dffi3  9382  card2inf  9508  elom3  9601  cantnfp1lem3  9633  cnfcomlem  9652  cnfcom  9653  cnfcom3  9657  ttrcltr  9669  ttrclselem1  9678  ttrclselem2  9679  finnum  9901  cardnn  9916  nnsdomel  9943  harsucnn  9951  nnadjuALT  10152  ficardun2  10155  ackbij1lem15  10186  ackbij2lem2  10192  ackbij2lem3  10193  ackbij2  10195  fin23lem22  10280  isf32lem5  10310  fin1a2lem4  10356  fin1a2lem9  10361  pwfseqlem3  10613  winainflem  10646  wunr1om  10672  tskr1om  10720  grothomex  10782  pion  10832  om2uzlt2i  13916  madefi  27824  oldfi  27825  precsexlem3  28111  precsexlem4  28112  precsexlem5  28113  om2noseqlt  28193  om2noseqlt2  28194  zs12bday  28343  constrfin  33736  constrextdg2lem  33738  constrext2chnlem  33740  constrfiss  33741  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  constrcn  33750  constrcjcl  33758  bnj168  34720  satfvsuc  35348  satf0suc  35363  sat1el2xp  35366  fmlasuc0  35371  elhf2  36163  findreccl  36441  rdgeqoa  37358  exrecfnlem  37367  finxpreclem4  37382  finxpreclem6  37384  harinf  43023  onexoegt  43233  oaabsb  43283  nnoeomeqom  43301  cantnfub  43310  dflim5  43318  onmcl  43320  omabs2  43321  tfsconcat0b  43335  naddcnffo  43353  naddonnn  43384  naddwordnexlem0  43385  naddwordnexlem3  43388  oawordex3  43389  naddwordnexlem4  43390  omssrncard  43529  nna1iscard  43534