Theorem nnon 7884

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Oncon0 6362  ωcom 7878

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-ss 3896  df-om 7879

This theorem is used by:  nnoni  7885  nnord  7886  peano4  7905  findsg  7910  onasuc  8540  onmsuc  8541  nna0  8617  nnm0  8618  nnasuc  8619  nnmsuc  8620  nnesuc  8621  nnecl  8626  nnawordi  8634  nnmword  8646  nnawordex  8650  nnaordex  8651  oaabslem  8660  oaabs  8661  oaabs2  8662  omabslem  8663  omabs  8664  nnneo  8668  nneob  8669  naddoa  8716  omnaddcl  8717  dif1ennn  9182  findcard2  9184  onfin2  9236  nndomo  9237  findcard3  9278  dffi3  9427  card2inf  9553  elom3  9653  cantnfp1lem3  9685  cnfcomlem  9704  cnfcom  9705  cnfcom3  9709  ttrcltr  9721  ttrclselem1  9730  ttrclselem2  9731  elhf2  9914  finnum  10033  cardnn  10048  nnsdomel  10075  harsucnn  10083  nnadjuALT  10281  ficardun2  10284  ackbij1lem15  10315  ackbij2lem2  10321  ackbij2lem3  10322  ackbij2  10324  fin23lem22  10409  isf32lem5  10439  fin1a2lem4  10485  fin1a2lem9  10490  pwfseqlem3  10749  winainflem  10782  wunr1om  10808  tskr1om  10856  grothomex  10918  pion  10968  om2uzlt2i  14098  madefi  28305  oldfi  28306  precsexlem3  28601  precsexlem4  28602  precsexlem5  28603  om2noseqlt  28691  om2noseqlt2  28692  constrfin  34425  constrextdg2lem  34427  constrext2chnlem  34429  constrfiss  34430  constrllcllem  34431  constrlccllem  34432  constrcccllem  34433  constrcn  34439  constrcjcl  34447  bnj168  35408  fineqvnttrclselem1  35846  fineqvnttrclselem2  35847  fineqvnttrclse  35849  kardnnfi  35894  satfvsuc  36213  satf0suc  36228  sat1el2xp  36231  fmlasuc0  36236  findreccl  37334  ttctr  37374  ttcmin  37377  dfttc2g  37387  rdgeqoa  38387  exrecfnlem  38396  finxpreclem4  38411  finxpreclem6  38413  harinf  44135  onexoegt  44340  oaabsb  44390  nnoeomeqom  44408  cantnfub  44417  dflim5  44425  onmcl  44427  omabs2  44428  tfsconcat0b  44442  naddcnffo  44460  naddonnn  44491  naddwordnexlem0  44492  naddwordnexlem3  44495  oawordex3  44496  naddwordnexlem4  44497  omssrncard  44635  nna1iscard  44640  hashnnsuc  46104  hashnnm  46105  hashnnltb  46107