Theorem nnon 7790

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

Syntax hints:   → wi 4   ∈ wcel 2106  Oncon0 6306  ωcom 7784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-in 3908  df-ss 3918  df-om 7785

This theorem is referenced by:  nnoni  7791  nnord  7792  peano4  7811  findsg  7818  onasuc  8433  onmsuc  8434  nna0  8510  nnm0  8511  nnasuc  8512  nnmsuc  8513  nnesuc  8514  nnecl  8519  nnawordi  8527  nnmword  8539  nnawordex  8543  nnaordex  8544  oaabslem  8552  oaabs  8553  oaabs2  8554  omabslem  8555  omabs  8556  nnneo  8560  nneob  8561  dif1ennn  9030  findcard2  9033  onfin2  9100  nndomo  9102  findcard3  9154  findcard3OLD  9155  dffi3  9292  card2inf  9416  elom3  9509  cantnfp1lem3  9541  cnfcomlem  9560  cnfcom  9561  cnfcom3  9565  ttrcltr  9577  ttrclselem1  9586  ttrclselem2  9587  finnum  9809  cardnn  9824  nnsdomel  9851  harsucnn  9859  nnadjuALT  10059  ficardun2  10063  ficardun2OLD  10064  ackbij1lem15  10095  ackbij2lem2  10101  ackbij2lem3  10102  ackbij2  10104  fin23lem22  10188  isf32lem5  10218  fin1a2lem4  10264  fin1a2lem9  10269  pwfseqlem3  10521  winainflem  10554  wunr1om  10580  tskr1om  10628  grothomex  10690  pion  10740  om2uzlt2i  13776  bnj168  33007  satfvsuc  33620  satf0suc  33635  sat1el2xp  33638  fmlasuc0  33643  elhf2  34614  findreccl  34779  rdgeqoa  35695  exrecfnlem  35704  finxpreclem4  35719  finxpreclem6  35721  harinf  41170  dflim5  41367  omabs2  41369  naddcnffo  41382  omssrncard  41521  nna1iscard  41526