Theorem nnon 7814

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

Syntax hints:   → wi 4   ∈ wcel 2113  Oncon0 6317  ωcom 7808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-ss 3918  df-om 7809

This theorem is referenced by:  nnoni  7815  nnord  7816  peano4  7834  findsg  7839  onasuc  8455  onmsuc  8456  nna0  8532  nnm0  8533  nnasuc  8534  nnmsuc  8535  nnesuc  8536  nnecl  8541  nnawordi  8549  nnmword  8561  nnawordex  8565  nnaordex  8566  oaabslem  8575  oaabs  8576  oaabs2  8577  omabslem  8578  omabs  8579  nnneo  8583  nneob  8584  naddoa  8630  omnaddcl  8631  dif1ennn  9087  findcard2  9089  onfin2  9141  nndomo  9142  findcard3  9183  dffi3  9334  card2inf  9460  elom3  9557  cantnfp1lem3  9589  cnfcomlem  9608  cnfcom  9609  cnfcom3  9613  ttrcltr  9625  ttrclselem1  9634  ttrclselem2  9635  finnum  9860  cardnn  9875  nnsdomel  9902  harsucnn  9910  nnadjuALT  10109  ficardun2  10112  ackbij1lem15  10143  ackbij2lem2  10149  ackbij2lem3  10150  ackbij2  10152  fin23lem22  10237  isf32lem5  10267  fin1a2lem4  10313  fin1a2lem9  10318  pwfseqlem3  10571  winainflem  10604  wunr1om  10630  tskr1om  10678  grothomex  10740  pion  10790  om2uzlt2i  13874  madefi  27909  oldfi  27910  precsexlem3  28205  precsexlem4  28206  precsexlem5  28207  om2noseqlt  28295  om2noseqlt2  28296  constrfin  33903  constrextdg2lem  33905  constrext2chnlem  33907  constrfiss  33908  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  constrcn  33917  constrcjcl  33925  bnj168  34886  fineqvnttrclselem1  35277  fineqvnttrclselem2  35278  fineqvnttrclse  35280  satfvsuc  35555  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  elhf2  36369  findreccl  36647  rdgeqoa  37575  exrecfnlem  37584  finxpreclem4  37599  finxpreclem6  37601  harinf  43276  onexoegt  43486  oaabsb  43536  nnoeomeqom  43554  cantnfub  43563  dflim5  43571  onmcl  43573  omabs2  43574  tfsconcat0b  43588  naddcnffo  43606  naddonnn  43637  naddwordnexlem0  43638  naddwordnexlem3  43641  oawordex3  43642  naddwordnexlem4  43643  omssrncard  43781  nna1iscard  43786