Theorem eloni 5988

Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)

Assertion

Ref	Expression
eloni	⊢ (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 5986	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 259	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 5977  Oncon0 5978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-uni 4674  df-tr 4990  df-po 5276  df-so 5277  df-fr 5316  df-we 5318  df-ord 5981  df-on 5982

This theorem is referenced by:  onelon  6003  onin  6009  ontri1  6012  onfr  6017  onelpss  6018  onsseleq  6019  onelss  6020  ontr1  6024  ontr2  6025  ordunidif  6026  on0eln0  6033  ordsssuc  6064  onsssuc  6065  onnbtwn  6069  suc11  6081  onordi  6082  onssneli  6087  epweon  7262  ordeleqon  7268  onss  7270  ordsuc  7294  onpwsuc  7296  onpsssuc  7299  onsucmin  7301  ordunpr  7306  ordunisuc  7312  onsucuni2  7314  onuninsuci  7320  ordunisuc2  7324  ordzsl  7325  onzsl  7326  nlimon  7331  tfinds  7339  tfindsg2  7341  nnord  7353  onfununi  7723  smo11  7746  smoord  7747  smoword  7748  smogt  7749  tfrlem1  7757  tfrlem9a  7767  tfrlem15  7773  tz7.44-2  7788  tz7.48lem  7821  oe0m1  7887  oaordi  7912  oaord  7913  oacan  7914  oawordri  7916  oalimcl  7926  oaass  7927  omord2  7933  omcan  7935  omwordi  7937  omword1  7939  omword2  7940  om00  7941  omlimcl  7944  omass  7946  omeulem2  7949  omopth2  7950  oen0  7952  oeord  7954  oecan  7955  oewordi  7957  oeworde  7959  oelimcl  7966  oeeulem  7967  oeeui  7968  nnarcl  7982  nnawordi  7987  nnawordex  8003  oaabs2  8011  omabs  8013  omsmo  8020  omxpenlem  8351  infensuc  8428  onomeneq  8440  ordiso  8712  ordtypelem2  8715  hartogslem1  8738  cantnflt  8868  cantnfp1lem3  8876  cantnfp1  8877  oemapso  8878  oemapvali  8880  cantnflem1d  8884  cantnflem1  8885  cantnf  8889  oemapwe  8890  cantnffval2  8891  cnfcom  8896  r111  8937  r1ordg  8940  rankonidlem  8990  bndrank  9003  r1pw  9007  r1pwALT  9008  rankbnd2  9031  tcrank  9046  cardprclem  9140  carduni  9142  cardmin2  9159  infxpenlem  9171  alephdom  9239  alephdom2  9245  cardaleph  9247  iscard3  9251  alephfp  9266  dfac12lem1  9302  dfac12lem2  9303  dfac12lem3  9304  cflim2  9422  cofsmo  9428  cfsmolem  9429  coftr  9432  cfcof  9433  fin67  9554  hsmexlem5  9589  zorn2lem6  9660  ttukeylem3  9670  ttukeylem5  9672  ttukeylem6  9673  ttukeylem7  9674  winainflem  9852  r1limwun  9895  r1wunlim  9896  tsksuc  9921  inar1  9934  gruina  9977  grur1a  9978  grur1  9979  dfrdg2  32297  poseq  32350  soseq  32351  nodmord  32403  noextendseq  32417  noextenddif  32418  nosupno  32446  nosupres  32450  noetalem3  32462  ontgval  33021  ontgsucval  33022  onsuctopon  33024  onintopssconn  33030  onsuct0  33031  sucneqond  33815  onsucuni3  33817  aomclem4  38600  aomclem5  38601  onfrALTlem3  39718  onfrALTlem2  39720  onfrALTlem3VD  40070  onfrALTlem2VD  40072  onsetreclem3  43572