Theorem nnon 7816

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

Syntax hints:   → wi 4   ∈ wcel 2114  Oncon0 6317  ωcom 7810

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 3391  df-ss 3907  df-om 7811

This theorem is referenced by:  nnoni  7817  nnord  7818  peano4  7836  findsg  7841  onasuc  8456  onmsuc  8457  nna0  8533  nnm0  8534  nnasuc  8535  nnmsuc  8536  nnesuc  8537  nnecl  8542  nnawordi  8550  nnmword  8562  nnawordex  8566  nnaordex  8567  oaabslem  8576  oaabs  8577  oaabs2  8578  omabslem  8579  omabs  8580  nnneo  8584  nneob  8585  naddoa  8631  omnaddcl  8632  dif1ennn  9090  findcard2  9092  onfin2  9144  nndomo  9145  findcard3  9186  dffi3  9337  card2inf  9463  elom3  9560  cantnfp1lem3  9592  cnfcomlem  9611  cnfcom  9612  cnfcom3  9616  ttrcltr  9628  ttrclselem1  9637  ttrclselem2  9638  finnum  9863  cardnn  9878  nnsdomel  9905  harsucnn  9913  nnadjuALT  10112  ficardun2  10115  ackbij1lem15  10146  ackbij2lem2  10152  ackbij2lem3  10153  ackbij2  10155  fin23lem22  10240  isf32lem5  10270  fin1a2lem4  10316  fin1a2lem9  10321  pwfseqlem3  10574  winainflem  10607  wunr1om  10633  tskr1om  10681  grothomex  10743  pion  10793  om2uzlt2i  13904  madefi  27919  oldfi  27920  precsexlem3  28215  precsexlem4  28216  precsexlem5  28217  om2noseqlt  28305  om2noseqlt2  28306  constrfin  33906  constrextdg2lem  33908  constrext2chnlem  33910  constrfiss  33911  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  constrcn  33920  constrcjcl  33928  bnj168  34889  fineqvnttrclselem1  35281  fineqvnttrclselem2  35282  fineqvnttrclse  35284  satfvsuc  35559  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  elhf2  36373  findreccl  36651  ttctr  36691  ttcmin  36694  dfttc2g  36704  rdgeqoa  37700  exrecfnlem  37709  finxpreclem4  37724  finxpreclem6  37726  harinf  43480  onexoegt  43690  oaabsb  43740  nnoeomeqom  43758  cantnfub  43767  dflim5  43775  onmcl  43777  omabs2  43778  tfsconcat0b  43792  naddcnffo  43810  naddonnn  43841  naddwordnexlem0  43842  naddwordnexlem3  43845  oawordex3  43846  naddwordnexlem4  43847  omssrncard  43985  nna1iscard  43990