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 3933	1 ⊢ (𝐴 ∈ ω → 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2143  Oncon0 6360  ωcom 7858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-ss 3922  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  10306  isf32lem5  10336  fin1a2lem4  10382  fin1a2lem9  10387  pwfseqlem3  10640  winainflem  10673  wunr1om  10699  tskr1om  10747  grothomex  10809  pion  10859  om2uzlt2i  13983  madefi  28106  oldfi  28107  precsexlem3  28402  precsexlem4  28403  precsexlem5  28404  om2noseqlt  28492  om2noseqlt2  28493  constrfin  34136  constrextdg2lem  34138  constrext2chnlem  34140  constrfiss  34141  constrllcllem  34142  constrlccllem  34143  constrcccllem  34144  constrcn  34150  constrcjcl  34158  bnj168  35119  fineqvnttrclselem1  35534  fineqvnttrclselem2  35535  fineqvnttrclse  35537  kardnnfi  35582  satfvsuc  35853  satf0suc  35868  sat1el2xp  35871  fmlasuc0  35876  elhf2  36667  findreccl  36964  ttctr  37004  ttcmin  37007  dfttc2g  37017  rdgeqoa  38016  exrecfnlem  38025  finxpreclem4  38040  finxpreclem6  38042  harinf  43761  onexoegt  43971  oaabsb  44021  nnoeomeqom  44039  cantnfub  44048  dflim5  44056  onmcl  44058  omabs2  44059  tfsconcat0b  44073  naddcnffo  44091  naddonnn  44122  naddwordnexlem0  44123  naddwordnexlem3  44126  oawordex3  44127  naddwordnexlem4  44128  omssrncard  44266  nna1iscard  44271  hashnnsuc  45729  hashnnm  45730  hashnnltb  45732