Theorem nnon 7823

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

Syntax hints:   → wi 4   ∈ wcel 2114  Oncon0 6323  ωcom 7817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-ss 3906  df-om 7818

This theorem is referenced by:  nnoni  7824  nnord  7825  peano4  7843  findsg  7848  onasuc  8463  onmsuc  8464  nna0  8540  nnm0  8541  nnasuc  8542  nnmsuc  8543  nnesuc  8544  nnecl  8549  nnawordi  8557  nnmword  8569  nnawordex  8573  nnaordex  8574  oaabslem  8583  oaabs  8584  oaabs2  8585  omabslem  8586  omabs  8587  nnneo  8591  nneob  8592  naddoa  8638  omnaddcl  8639  dif1ennn  9097  findcard2  9099  onfin2  9151  nndomo  9152  findcard3  9193  dffi3  9344  card2inf  9470  elom3  9569  cantnfp1lem3  9601  cnfcomlem  9620  cnfcom  9621  cnfcom3  9625  ttrcltr  9637  ttrclselem1  9646  ttrclselem2  9647  finnum  9872  cardnn  9887  nnsdomel  9914  harsucnn  9922  nnadjuALT  10121  ficardun2  10124  ackbij1lem15  10155  ackbij2lem2  10161  ackbij2lem3  10162  ackbij2  10164  fin23lem22  10249  isf32lem5  10279  fin1a2lem4  10325  fin1a2lem9  10330  pwfseqlem3  10583  winainflem  10616  wunr1om  10642  tskr1om  10690  grothomex  10752  pion  10802  om2uzlt2i  13913  madefi  27905  oldfi  27906  precsexlem3  28201  precsexlem4  28202  precsexlem5  28203  om2noseqlt  28291  om2noseqlt2  28292  constrfin  33890  constrextdg2lem  33892  constrext2chnlem  33894  constrfiss  33895  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  constrcn  33904  constrcjcl  33912  bnj168  34873  fineqvnttrclselem1  35265  fineqvnttrclselem2  35266  fineqvnttrclse  35268  satfvsuc  35543  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  elhf2  36357  findreccl  36635  ttctr  36675  ttcmin  36678  dfttc2g  36688  rdgeqoa  37686  exrecfnlem  37695  finxpreclem4  37710  finxpreclem6  37712  harinf  43462  onexoegt  43672  oaabsb  43722  nnoeomeqom  43740  cantnfub  43749  dflim5  43757  onmcl  43759  omabs2  43760  tfsconcat0b  43774  naddcnffo  43792  naddonnn  43823  naddwordnexlem0  43824  naddwordnexlem3  43827  oawordex3  43828  naddwordnexlem4  43829  omssrncard  43967  nna1iscard  43972