Theorem nnon 7442

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

Syntax hints:   → wi 4   ∈ wcel 2081  Oncon0 6066  ωcom 7436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-tr 5064  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-om 7437

This theorem is referenced by:  nnoni  7443  nnord  7444  peano4  7460  findsg  7465  onasuc  8004  onmsuc  8005  nna0  8080  nnm0  8081  nnasuc  8082  nnmsuc  8083  nnesuc  8084  nnecl  8089  nnawordi  8097  nnmword  8109  nnawordex  8113  nnaordex  8114  oaabslem  8120  oaabs  8121  oaabs2  8122  omabslem  8123  omabs  8124  nnneo  8128  nneob  8129  onfin2  8556  findcard3  8607  dffi3  8741  card2inf  8865  elom3  8957  cantnfp1lem3  8989  cnfcomlem  9008  cnfcom  9009  cnfcom3  9013  finnum  9223  cardnn  9238  nnsdomel  9265  nnadju  9469  ficardun2  9471  ackbij1lem15  9502  ackbij2lem2  9508  ackbij2lem3  9509  ackbij2  9511  fin23lem22  9595  isf32lem5  9625  fin1a2lem4  9671  fin1a2lem9  9676  pwfseqlem3  9928  winainflem  9961  wunr1om  9987  tskr1om  10035  grothomex  10097  pion  10147  om2uzlt2i  13169  bnj168  31617  satfvsuc  32216  satf0suc  32231  sat1el2xp  32234  fmlasuc0  32239  elhf2  33245  findreccl  33410  rdgeqoa  34182  exrecfnlem  34191  finxpreclem4  34206  finxpreclem6  34208  harinf  39116  harsucnn  39388