Theorem nnon 7847

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

Syntax hints:   → wi 4   ∈ wcel 2141  Oncon0 6341  ωcom 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-ss 3919  df-om 7842

This theorem is referenced by:  nnoni  7848  nnord  7849  peano4  7868  findsg  7873  onasuc  8491  onmsuc  8492  nna0  8568  nnm0  8569  nnasuc  8570  nnmsuc  8571  nnesuc  8572  nnecl  8577  nnawordi  8585  nnmword  8597  nnawordex  8601  nnaordex  8602  oaabslem  8611  oaabs  8612  oaabs2  8613  omabslem  8614  omabs  8615  nnneo  8619  nneob  8620  naddoa  8667  omnaddcl  8668  dif1ennn  9125  findcard2  9127  onfin2  9179  nndomo  9180  findcard3  9221  dffi3  9371  card2inf  9497  elom3  9597  cantnfp1lem3  9629  cnfcomlem  9648  cnfcom  9649  cnfcom3  9653  ttrcltr  9665  ttrclselem1  9674  ttrclselem2  9675  finnum  9900  cardnn  9915  nnsdomel  9942  harsucnn  9950  nnadjuALT  10149  ficardun2  10152  ackbij1lem15  10183  ackbij2lem2  10189  ackbij2lem3  10190  ackbij2  10192  fin23lem22  10278  isf32lem5  10308  fin1a2lem4  10354  fin1a2lem9  10359  pwfseqlem3  10612  winainflem  10645  wunr1om  10671  tskr1om  10719  grothomex  10781  pion  10831  om2uzlt2i  13958  madefi  27994  oldfi  27995  precsexlem3  28290  precsexlem4  28291  precsexlem5  28292  om2noseqlt  28380  om2noseqlt2  28381  constrfin  34004  constrextdg2lem  34006  constrext2chnlem  34008  constrfiss  34009  constrllcllem  34010  constrlccllem  34011  constrcccllem  34012  constrcn  34018  constrcjcl  34026  bnj168  34987  fineqvnttrclselem1  35378  fineqvnttrclselem2  35379  fineqvnttrclse  35381  satfvsuc  35672  satf0suc  35687  sat1el2xp  35690  fmlasuc0  35695  elhf2  36486  findreccl  36774  ttctr  36814  ttcmin  36817  dfttc2g  36827  rdgeqoa  37825  exrecfnlem  37834  finxpreclem4  37849  finxpreclem6  37851  harinf  43572  onexoegt  43782  oaabsb  43832  nnoeomeqom  43850  cantnfub  43859  dflim5  43867  onmcl  43869  omabs2  43870  tfsconcat0b  43884  naddcnffo  43902  naddonnn  43933  naddwordnexlem0  43934  naddwordnexlem3  43937  oawordex3  43938  naddwordnexlem4  43939  omssrncard  44077  nna1iscard  44082