Theorem eloni 6332

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

Syntax hints:   → wi 4   ∈ wcel 2106  Ord word 6321  Oncon0 6322

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871  df-tr 5228  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-ord 6325  df-on 6326

This theorem is referenced by:  onelon  6347  onin  6353  ontri1  6356  onfr  6361  onelpss  6362  onsseleq  6363  onelss  6364  ontr1  6368  ontr2  6369  ordunidif  6371  on0eln0  6378  ordsssuc  6411  onsssuc  6412  onnbtwn  6416  onunel  6427  suc11  6429  onun2  6430  ontr  6431  onordi  6433  onssneli  6438  epweon  7714  epweonALT  7715  ordeleqon  7721  onss  7724  sucexeloni  7749  ordsucOLD  7754  onpwsuc  7756  onpsssuc  7759  onsucmin  7761  ordunpr  7766  ordunisuc  7772  onsucuni2  7774  onuniorsuc  7777  ordunisuc2  7785  ordzsl  7786  onzsl  7787  nlimon  7792  tfinds  7801  tfindsg2  7803  nnord  7815  poseq  8095  soseq  8096  onfununi  8292  smo11  8315  smoord  8316  smoword  8317  smogt  8318  tfrlem1  8327  tfrlem9a  8337  tfrlem15  8343  tz7.44-2  8358  tz7.48lem  8392  ord3  8434  oe0m1  8472  oaordi  8498  oaord  8499  oacan  8500  oawordri  8502  oalimcl  8512  oaass  8513  omord2  8519  omcan  8521  omwordi  8523  omword1  8525  omword2  8526  om00  8527  omlimcl  8530  omass  8532  omeulem2  8535  omopth2  8536  oen0  8538  oeord  8540  oecan  8541  oewordi  8543  oeworde  8545  oelimcl  8552  oeeulem  8553  oeeui  8554  nnarcl  8568  nnawordi  8573  nnawordex  8589  oaabs2  8600  omabs  8602  omsmo  8609  cofonr  8625  naddcllem  8627  omxpenlem  9024  infensuc  9106  dif1enlem  9107  nndomog  9167  nndomogOLD  9177  onomeneq  9179  onomeneqOLD  9180  ordiso  9461  ordtypelem2  9464  hartogslem1  9487  cantnflt  9617  cantnfp1lem3  9625  cantnfp1  9626  oemapso  9627  oemapvali  9629  cantnflem1d  9633  cantnflem1  9634  cantnf  9638  oemapwe  9639  cantnffval2  9640  cnfcom  9645  r111  9720  r1ordg  9723  rankonidlem  9773  bndrank  9786  r1pw  9790  r1pwALT  9791  rankbnd2  9814  tcrank  9829  cardprclem  9924  carduni  9926  cardmin2  9944  infxpenlem  9958  alephdom  10026  alephdom2  10032  cardaleph  10034  iscard3  10038  alephfp  10053  dfac12lem1  10088  dfac12lem2  10089  dfac12lem3  10090  cflim2  10208  cofsmo  10214  cfsmolem  10215  coftr  10218  cfcof  10219  fin67  10340  hsmexlem5  10375  zorn2lem6  10446  ttukeylem3  10456  ttukeylem5  10458  ttukeylem6  10459  ttukeylem7  10460  winainflem  10638  r1limwun  10681  r1wunlim  10682  tsksuc  10707  inar1  10720  gruina  10763  grur1a  10764  grur1  10765  nodmord  27038  noextendseq  27052  noextenddif  27053  nosupno  27088  nosupbday  27090  nosupres  27092  noinfno  27103  noinfbday  27105  noinfres  27107  noetasuplem4  27121  noetainflem4  27125  newbday  27274  dfrdg2  34456  ontgval  34979  ontgsucval  34980  onsuctopon  34982  onintopssconn  34988  onsuct0  34989  sucneqond  35909  onsucuni3  35911  aomclem4  41442  aomclem5  41443  onintunirab  41619  omlimcl2  41634  onelord  41643  oneltri  41650  ordeldifsucon  41652  ordeldif1o  41653  onsucss  41659  onsucf1olem  41663  onov0suclim  41667  oe0rif  41678  onsucwordi  41681  oege1  41699  cantnfresb  41717  omabs2  41725  ordsssucb  41728  tfsconcatlem  41729  tfsconcatfv2  41733  tfsconcatrn  41735  tfsconcatb0  41737  tfsconcat0b  41739  tfsconcatrev  41741  onsucunipr  41765  oaun3lem1  41767  oaun3lem2  41768  nadd1suc  41785  naddsuc2  41786  naddgeoa  41788  oaltom  41799  omltoe  41801  nlimsuc  41835  dfsucon  41917  minregex  41928  onfrALTlem3  42948  onfrALTlem2  42950  onfrALTlem3VD  43291  onfrALTlem2VD  43293  onsetreclem3  47272