Theorem nnon 7872

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

Syntax hints:   → wi 4   ∈ wcel 2109  Oncon0 6357  ωcom 7866

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-ss 3948  df-om 7867

This theorem is referenced by:  nnoni  7873  nnord  7874  peano4  7893  findsg  7898  onasuc  8545  onmsuc  8546  nna0  8621  nnm0  8622  nnasuc  8623  nnmsuc  8624  nnesuc  8625  nnecl  8630  nnawordi  8638  nnmword  8650  nnawordex  8654  nnaordex  8655  oaabslem  8664  oaabs  8665  oaabs2  8666  omabslem  8667  omabs  8668  nnneo  8672  nneob  8673  naddoa  8719  omnaddcl  8720  dif1ennn  9180  findcard2  9183  onfin2  9245  nndomo  9246  findcard3  9295  findcard3OLD  9296  dffi3  9448  card2inf  9574  elom3  9667  cantnfp1lem3  9699  cnfcomlem  9718  cnfcom  9719  cnfcom3  9723  ttrcltr  9735  ttrclselem1  9744  ttrclselem2  9745  finnum  9967  cardnn  9982  nnsdomel  10009  harsucnn  10017  nnadjuALT  10218  ficardun2  10221  ackbij1lem15  10252  ackbij2lem2  10258  ackbij2lem3  10259  ackbij2  10261  fin23lem22  10346  isf32lem5  10376  fin1a2lem4  10422  fin1a2lem9  10427  pwfseqlem3  10679  winainflem  10712  wunr1om  10738  tskr1om  10786  grothomex  10848  pion  10898  om2uzlt2i  13974  madefi  27881  oldfi  27882  precsexlem3  28168  precsexlem4  28169  precsexlem5  28170  om2noseqlt  28250  om2noseqlt2  28251  zs12bday  28400  constrfin  33785  constrextdg2lem  33787  constrext2chnlem  33789  constrfiss  33790  constrllcllem  33791  constrlccllem  33792  constrcccllem  33793  constrcn  33799  constrcjcl  33807  bnj168  34766  satfvsuc  35388  satf0suc  35403  sat1el2xp  35406  fmlasuc0  35411  elhf2  36198  findreccl  36476  rdgeqoa  37393  exrecfnlem  37402  finxpreclem4  37417  finxpreclem6  37419  harinf  43025  onexoegt  43235  oaabsb  43285  nnoeomeqom  43303  cantnfub  43312  dflim5  43320  onmcl  43322  omabs2  43323  tfsconcat0b  43337  naddcnffo  43355  naddonnn  43386  naddwordnexlem0  43387  naddwordnexlem3  43390  oawordex3  43391  naddwordnexlem4  43392  omssrncard  43531  nna1iscard  43536