Theorem eloni 6395

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 6393	. 2 ⊢ (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
2	1	ibi 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2105  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-v 3479  df-ss 3979  df-uni 4912  df-tr 5265  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  onelon  6410  onin  6416  ontri1  6419  onfr  6424  onelpss  6425  onsseleq  6426  onelss  6427  ontr1  6431  ontr2  6432  ordunidif  6434  on0eln0  6441  ordsssuc  6474  onsssuc  6475  onnbtwn  6479  onunel  6490  suc11  6492  onun2  6493  ontr  6494  onordi  6496  onssneli  6501  epweon  7793  epweonALT  7794  ordeleqon  7800  onss  7803  sucexeloni  7828  ordsucOLD  7833  onpwsuc  7835  onpsssuc  7838  onsucmin  7840  ordunpr  7845  ordunisuc  7851  onsucuni2  7853  onuniorsuc  7856  ordunisuc2  7864  ordzsl  7865  onzsl  7866  nlimon  7871  tfinds  7880  tfindsg2  7882  nnord  7894  poseq  8181  soseq  8182  onfununi  8379  smo11  8402  smoord  8403  smoword  8404  smogt  8405  tfrlem1  8414  tfrlem9a  8424  tfrlem15  8430  tz7.44-2  8445  tz7.48lem  8479  ord3  8521  oe0m1  8557  oaordi  8582  oaord  8583  oacan  8584  oawordri  8586  oalimcl  8596  oaass  8597  omord2  8603  omcan  8605  omwordi  8607  omword1  8609  omword2  8610  om00  8611  omlimcl  8614  omass  8616  omeulem2  8619  omopth2  8620  oen0  8622  oeord  8624  oecan  8625  oewordi  8627  oeworde  8629  oelimcl  8636  oeeulem  8637  oeeui  8638  nnarcl  8652  nnawordi  8657  nnawordex  8673  oaabs2  8685  omabs  8687  omsmo  8694  cofonr  8710  naddcllem  8712  naddsuc2  8737  omxpenlem  9111  infensuc  9193  dif1enlem  9194  nndomog  9250  nndomogOLD  9260  onomeneq  9262  onomeneqOLD  9263  ordiso  9553  ordtypelem2  9556  hartogslem1  9579  cantnflt  9709  cantnfp1lem3  9717  cantnfp1  9718  oemapso  9719  oemapvali  9721  cantnflem1d  9725  cantnflem1  9726  cantnf  9730  oemapwe  9731  cantnffval2  9732  cnfcom  9737  r111  9812  r1ordg  9815  rankonidlem  9865  bndrank  9878  r1pw  9882  r1pwALT  9883  rankbnd2  9906  tcrank  9921  cardprclem  10016  carduni  10018  cardmin2  10036  infxpenlem  10050  alephdom  10118  alephdom2  10124  cardaleph  10126  iscard3  10130  alephfp  10145  dfac12lem1  10181  dfac12lem2  10182  dfac12lem3  10183  cflim2  10300  cofsmo  10306  cfsmolem  10307  coftr  10310  cfcof  10311  fin67  10432  hsmexlem5  10467  zorn2lem6  10538  ttukeylem3  10548  ttukeylem5  10550  ttukeylem6  10551  ttukeylem7  10552  winainflem  10730  r1limwun  10773  r1wunlim  10774  tsksuc  10799  inar1  10812  gruina  10855  grur1a  10856  grur1  10857  nodmord  27712  noextendseq  27726  noextenddif  27727  nosupno  27762  nosupbday  27764  nosupres  27766  noinfno  27777  noinfbday  27779  noinfres  27781  noetasuplem4  27795  noetainflem4  27799  newbday  27954  dfrdg2  35776  ontgval  36413  ontgsucval  36414  onsuctopon  36416  onintopssconn  36422  onsuct0  36423  sucneqond  37347  onsucuni3  37349  aomclem4  43045  aomclem5  43046  onintunirab  43215  omlimcl2  43230  onelord  43239  oneltri  43246  ordeldifsucon  43248  ordeldif1o  43249  onsucss  43255  onsucf1olem  43259  onov0suclim  43263  oe0rif  43274  onsucwordi  43277  oege1  43295  cantnfresb  43313  omabs2  43321  ordsssucb  43324  tfsconcatlem  43325  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  tfsconcat0b  43335  tfsconcatrev  43337  onsucunipr  43361  oaun3lem1  43363  oaun3lem2  43364  nadd1suc  43381  naddgeoa  43383  oaltom  43394  omltoe  43396  nlimsuc  43430  dfsucon  43512  minregex  43523  onfrALTlem3  44541  onfrALTlem2  44543  onfrALTlem3VD  44884  onfrALTlem2VD  44886  onsetreclem3  48937