Theorem nnon 7693

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

Syntax hints:   → wi 4   ∈ wcel 2108  Oncon0 6251  ωcom 7687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-om 7688

This theorem is referenced by:  nnoni  7694  nnord  7695  peano4  7713  findsg  7720  onasuc  8320  onmsuc  8321  nna0  8397  nnm0  8398  nnasuc  8399  nnmsuc  8400  nnesuc  8401  nnecl  8406  nnawordi  8414  nnmword  8426  nnawordex  8430  nnaordex  8431  oaabslem  8437  oaabs  8438  oaabs2  8439  omabslem  8440  omabs  8441  nnneo  8445  nneob  8446  onfin2  8945  nndomo  8947  findcard3  8987  dffi3  9120  card2inf  9244  elom3  9336  cantnfp1lem3  9368  cnfcomlem  9387  cnfcom  9388  cnfcom3  9392  finnum  9637  cardnn  9652  nnsdomel  9679  harsucnn  9687  nnadjuALT  9885  ficardun2  9889  ficardun2OLD  9890  ackbij1lem15  9921  ackbij2lem2  9927  ackbij2lem3  9928  ackbij2  9930  fin23lem22  10014  isf32lem5  10044  fin1a2lem4  10090  fin1a2lem9  10095  pwfseqlem3  10347  winainflem  10380  wunr1om  10406  tskr1om  10454  grothomex  10516  pion  10566  om2uzlt2i  13599  bnj168  32609  satfvsuc  33223  satf0suc  33238  sat1el2xp  33241  fmlasuc0  33246  ttrcltr  33702  ttrclselem1  33711  ttrclselem2  33712  elhf2  34404  findreccl  34569  rdgeqoa  35468  exrecfnlem  35477  finxpreclem4  35492  finxpreclem6  35494  harinf  40772