Theorem nnon 7797

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

Syntax hints:   → wi 4   ∈ wcel 2111  Oncon0 6301  ωcom 7791

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-ss 3914  df-om 7792

This theorem is referenced by:  nnoni  7798  nnord  7799  peano4  7817  findsg  7822  onasuc  8438  onmsuc  8439  nna0  8514  nnm0  8515  nnasuc  8516  nnmsuc  8517  nnesuc  8518  nnecl  8523  nnawordi  8531  nnmword  8543  nnawordex  8547  nnaordex  8548  oaabslem  8557  oaabs  8558  oaabs2  8559  omabslem  8560  omabs  8561  nnneo  8565  nneob  8566  naddoa  8612  omnaddcl  8613  dif1ennn  9067  findcard2  9069  onfin2  9120  nndomo  9121  findcard3  9162  dffi3  9310  card2inf  9436  elom3  9533  cantnfp1lem3  9565  cnfcomlem  9584  cnfcom  9585  cnfcom3  9589  ttrcltr  9601  ttrclselem1  9610  ttrclselem2  9611  finnum  9836  cardnn  9851  nnsdomel  9878  harsucnn  9886  nnadjuALT  10085  ficardun2  10088  ackbij1lem15  10119  ackbij2lem2  10125  ackbij2lem3  10126  ackbij2  10128  fin23lem22  10213  isf32lem5  10243  fin1a2lem4  10289  fin1a2lem9  10294  pwfseqlem3  10546  winainflem  10579  wunr1om  10605  tskr1om  10653  grothomex  10715  pion  10765  om2uzlt2i  13853  madefi  27853  oldfi  27854  precsexlem3  28142  precsexlem4  28143  precsexlem5  28144  om2noseqlt  28224  om2noseqlt2  28225  zs12bday  28389  constrfin  33751  constrextdg2lem  33753  constrext2chnlem  33755  constrfiss  33756  constrllcllem  33757  constrlccllem  33758  constrcccllem  33759  constrcn  33765  constrcjcl  33773  bnj168  34734  fineqvnttrclselem1  35133  fineqvnttrclselem2  35134  fineqvnttrclse  35136  satfvsuc  35397  satf0suc  35412  sat1el2xp  35415  fmlasuc0  35420  elhf2  36209  findreccl  36487  rdgeqoa  37404  exrecfnlem  37413  finxpreclem4  37428  finxpreclem6  37430  harinf  43067  onexoegt  43277  oaabsb  43327  nnoeomeqom  43345  cantnfub  43354  dflim5  43362  onmcl  43364  omabs2  43365  tfsconcat0b  43379  naddcnffo  43397  naddonnn  43428  naddwordnexlem0  43429  naddwordnexlem3  43432  oawordex3  43433  naddwordnexlem4  43434  omssrncard  43573  nna1iscard  43578