Theorem nnon 7917

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Oncon0 6388  ωcom 7911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-ss 3901  df-om 7912

This theorem is used by:  nnoni  7918  nnord  7919  peano4  7938  findsg  7943  onasuc  8574  onmsuc  8575  nna0  8651  nnm0  8652  nnasuc  8653  nnmsuc  8654  nnesuc  8655  nnecl  8660  nnawordi  8668  nnmword  8680  nnawordex  8684  nnaordex  8685  oaabslem  8694  oaabs  8695  oaabs2  8696  omabslem  8697  omabs  8698  nnneo  8702  nneob  8703  naddoa  8750  omnaddcl  8751  dif1ennn  9216  findcard2  9218  onfin2  9270  nndomo  9271  findcard3  9312  dffi3  9460  card2inf  9586  elom3  9686  cantnfp1lem3  9718  cnfcomlem  9737  cnfcom  9738  cnfcom3  9742  ttrcltr  9754  ttrclselem1  9763  ttrclselem2  9764  elhf2  9947  finnum  10066  cardnn  10081  nnsdomel  10110  harsucnn  10118  nnadjuALT  10316  ficardun2  10319  ackbij1lem15  10350  ackbij2lem2  10356  ackbij2lem3  10357  ackbij2  10359  fin23lem22  10444  isf32lem5  10474  fin1a2lem4  10520  fin1a2lem9  10525  pwfseqlem3  10784  winainflem  10817  wunr1om  10843  tskr1om  10891  grothomex  10953  pion  11003  om2uzlt2i  14134  madefi  28356  oldfi  28357  precsexlem3  28652  precsexlem4  28653  precsexlem5  28654  om2noseqlt  28742  om2noseqlt2  28743  constrfin  34489  constrextdg2lem  34491  constrext2chnlem  34493  constrfiss  34494  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  constrcn  34503  constrcjcl  34511  bnj168  35472  fineqvnttrclselem1  35930  fineqvnttrclselem2  35931  fineqvnttrclse  35933  kardnnfi  35978  satfvsuc  36334  satf0suc  36349  sat1el2xp  36352  fmlasuc0  36357  findreccl  37456  ttctr  37496  ttcmin  37499  dfttc2g  37509  rdgeqoa  38561  exrecfnlem  38570  finxpreclem4  38585  finxpreclem6  38587  harinf  44307  onexoegt  44507  oaabsb  44557  nnoeomeqom  44575  cantnfub  44584  dflim5  44592  onmcl  44594  omabs2  44595  tfsconcat0b  44609  naddcnffo  44627  naddonnn  44658  naddwordnexlem0  44659  naddwordnexlem3  44662  oawordex3  44663  naddwordnexlem4  44664  omssrncard  44802  nna1iscard  44807  hashnnsuc  46274  hashnnm  46275  hashnnltb  46277