Theorem nnon 7864

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

Syntax hints:   → wi 4   ∈ wcel 2149  Oncon0 6358  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-ss 3930  df-om 7859

This theorem is referenced by:  nnoni  7865  nnord  7866  peano4  7885  findsg  7890  onasuc  8509  onmsuc  8510  nna0  8586  nnm0  8587  nnasuc  8588  nnmsuc  8589  nnesuc  8590  nnecl  8595  nnawordi  8603  nnmword  8615  nnawordex  8619  nnaordex  8620  oaabslem  8629  oaabs  8630  oaabs2  8631  omabslem  8632  omabs  8633  nnneo  8637  nneob  8638  naddoa  8685  omnaddcl  8686  dif1ennn  9143  findcard2  9145  onfin2  9197  nndomo  9198  findcard3  9239  dffi3  9387  card2inf  9513  elom3  9613  cantnfp1lem3  9645  cnfcomlem  9664  cnfcom  9665  cnfcom3  9669  ttrcltr  9681  ttrclselem1  9690  ttrclselem2  9691  finnum  9930  cardnn  9945  nnsdomel  9972  harsucnn  9980  nnadjuALT  10178  ficardun2  10181  ackbij1lem15  10212  ackbij2lem2  10218  ackbij2lem3  10219  ackbij2  10221  fin23lem22  10307  isf32lem5  10337  fin1a2lem4  10383  fin1a2lem9  10388  pwfseqlem3  10641  winainflem  10674  wunr1om  10700  tskr1om  10748  grothomex  10810  pion  10860  om2uzlt2i  13983  madefi  28068  oldfi  28069  precsexlem3  28364  precsexlem4  28365  precsexlem5  28366  om2noseqlt  28454  om2noseqlt2  28455  constrfin  34077  constrextdg2lem  34079  constrext2chnlem  34081  constrfiss  34082  constrllcllem  34083  constrlccllem  34084  constrcccllem  34085  constrcn  34091  constrcjcl  34099  bnj168  35060  fineqvnttrclselem1  35453  fineqvnttrclselem2  35454  fineqvnttrclse  35456  satfvsuc  35748  satf0suc  35763  sat1el2xp  35766  fmlasuc0  35771  elhf2  36562  findreccl  36849  ttctr  36889  ttcmin  36892  dfttc2g  36902  rdgeqoa  37899  exrecfnlem  37908  finxpreclem4  37923  finxpreclem6  37925  harinf  43648  onexoegt  43858  oaabsb  43908  nnoeomeqom  43926  cantnfub  43935  dflim5  43943  onmcl  43945  omabs2  43946  tfsconcat0b  43960  naddcnffo  43978  naddonnn  44009  naddwordnexlem0  44010  naddwordnexlem3  44013  oawordex3  44014  naddwordnexlem4  44015  omssrncard  44153  nna1iscard  44158  hashnnsuc  45616  hashnnm  45617  hashnnltb  45619