Theorem nnon 7824

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

Syntax hints:   → wi 4   ∈ wcel 2114  Oncon0 6325  ωcom 7818

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-ss 3920  df-om 7819

This theorem is referenced by:  nnoni  7825  nnord  7826  peano4  7844  findsg  7849  onasuc  8465  onmsuc  8466  nna0  8542  nnm0  8543  nnasuc  8544  nnmsuc  8545  nnesuc  8546  nnecl  8551  nnawordi  8559  nnmword  8571  nnawordex  8575  nnaordex  8576  oaabslem  8585  oaabs  8586  oaabs2  8587  omabslem  8588  omabs  8589  nnneo  8593  nneob  8594  naddoa  8640  omnaddcl  8641  dif1ennn  9099  findcard2  9101  onfin2  9153  nndomo  9154  findcard3  9195  dffi3  9346  card2inf  9472  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  13886  madefi  27921  oldfi  27922  precsexlem3  28217  precsexlem4  28218  precsexlem5  28219  om2noseqlt  28307  om2noseqlt2  28308  constrfin  33924  constrextdg2lem  33926  constrext2chnlem  33928  constrfiss  33929  constrllcllem  33930  constrlccllem  33931  constrcccllem  33932  constrcn  33938  constrcjcl  33946  bnj168  34907  fineqvnttrclselem1  35299  fineqvnttrclselem2  35300  fineqvnttrclse  35302  satfvsuc  35577  satf0suc  35592  sat1el2xp  35595  fmlasuc0  35600  elhf2  36391  findreccl  36669  rdgeqoa  37625  exrecfnlem  37634  finxpreclem4  37649  finxpreclem6  37651  harinf  43391  onexoegt  43601  oaabsb  43651  nnoeomeqom  43669  cantnfub  43678  dflim5  43686  onmcl  43688  omabs2  43689  tfsconcat0b  43703  naddcnffo  43721  naddonnn  43752  naddwordnexlem0  43753  naddwordnexlem3  43756  oawordex3  43757  naddwordnexlem4  43758  omssrncard  43896  nna1iscard  43901