Theorem nnon 7851

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

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6335  ωcom 7845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-om 7846

This theorem is referenced by:  nnoni  7852  nnord  7853  peano4  7871  findsg  7876  onasuc  8495  onmsuc  8496  nna0  8571  nnm0  8572  nnasuc  8573  nnmsuc  8574  nnesuc  8575  nnecl  8580  nnawordi  8588  nnmword  8600  nnawordex  8604  nnaordex  8605  oaabslem  8614  oaabs  8615  oaabs2  8616  omabslem  8617  omabs  8618  nnneo  8622  nneob  8623  naddoa  8669  omnaddcl  8670  dif1ennn  9131  findcard2  9134  onfin2  9186  nndomo  9187  findcard3  9236  findcard3OLD  9237  dffi3  9389  card2inf  9515  elom3  9608  cantnfp1lem3  9640  cnfcomlem  9659  cnfcom  9660  cnfcom3  9664  ttrcltr  9676  ttrclselem1  9685  ttrclselem2  9686  finnum  9908  cardnn  9923  nnsdomel  9950  harsucnn  9958  nnadjuALT  10159  ficardun2  10162  ackbij1lem15  10193  ackbij2lem2  10199  ackbij2lem3  10200  ackbij2  10202  fin23lem22  10287  isf32lem5  10317  fin1a2lem4  10363  fin1a2lem9  10368  pwfseqlem3  10620  winainflem  10653  wunr1om  10679  tskr1om  10727  grothomex  10789  pion  10839  om2uzlt2i  13923  madefi  27831  oldfi  27832  precsexlem3  28118  precsexlem4  28119  precsexlem5  28120  om2noseqlt  28200  om2noseqlt2  28201  zs12bday  28350  constrfin  33743  constrextdg2lem  33745  constrext2chnlem  33747  constrfiss  33748  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  constrcn  33757  constrcjcl  33765  bnj168  34727  satfvsuc  35355  satf0suc  35370  sat1el2xp  35373  fmlasuc0  35378  elhf2  36170  findreccl  36448  rdgeqoa  37365  exrecfnlem  37374  finxpreclem4  37389  finxpreclem6  37391  harinf  43030  onexoegt  43240  oaabsb  43290  nnoeomeqom  43308  cantnfub  43317  dflim5  43325  onmcl  43327  omabs2  43328  tfsconcat0b  43342  naddcnffo  43360  naddonnn  43391  naddwordnexlem0  43392  naddwordnexlem3  43395  oawordex3  43396  naddwordnexlem4  43397  omssrncard  43536  nna1iscard  43541