Theorem eloni 6394

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6383  Oncon0 6384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-ord 6387  df-on 6388

This theorem is referenced by:  onelon  6409  onin  6415  ontri1  6418  onfr  6423  onelpss  6424  onsseleq  6425  onelss  6426  ontr1  6430  ontr2  6431  ordunidif  6433  on0eln0  6440  ordsssuc  6473  onsssuc  6474  onnbtwn  6478  onunel  6489  suc11  6491  onun2  6492  ontr  6493  onordi  6495  onssneli  6500  epweon  7795  epweonALT  7796  ordeleqon  7802  onss  7805  sucexeloni  7829  ordsucOLD  7834  onpwsuc  7836  onpsssuc  7839  onsucmin  7841  ordunpr  7846  ordunisuc  7852  onsucuni2  7854  onuniorsuc  7857  ordunisuc2  7865  ordzsl  7866  onzsl  7867  nlimon  7872  tfinds  7881  tfindsg2  7883  nnord  7895  poseq  8183  soseq  8184  onfununi  8381  smo11  8404  smoord  8405  smoword  8406  smogt  8407  tfrlem1  8416  tfrlem9a  8426  tfrlem15  8432  tz7.44-2  8447  tz7.48lem  8481  ord3  8523  oe0m1  8559  oaordi  8584  oaord  8585  oacan  8586  oawordri  8588  oalimcl  8598  oaass  8599  omord2  8605  omcan  8607  omwordi  8609  omword1  8611  omword2  8612  om00  8613  omlimcl  8616  omass  8618  omeulem2  8621  omopth2  8622  oen0  8624  oeord  8626  oecan  8627  oewordi  8629  oeworde  8631  oelimcl  8638  oeeulem  8639  oeeui  8640  nnarcl  8654  nnawordi  8659  nnawordex  8675  oaabs2  8687  omabs  8689  omsmo  8696  cofonr  8712  naddcllem  8714  naddsuc2  8739  omxpenlem  9113  infensuc  9195  dif1enlem  9196  nndomog  9253  nndomogOLD  9263  onomeneq  9265  onomeneqOLD  9266  ordiso  9556  ordtypelem2  9559  hartogslem1  9582  cantnflt  9712  cantnfp1lem3  9720  cantnfp1  9721  oemapso  9722  oemapvali  9724  cantnflem1d  9728  cantnflem1  9729  cantnf  9733  oemapwe  9734  cantnffval2  9735  cnfcom  9740  r111  9815  r1ordg  9818  rankonidlem  9868  bndrank  9881  r1pw  9885  r1pwALT  9886  rankbnd2  9909  tcrank  9924  cardprclem  10019  carduni  10021  cardmin2  10039  infxpenlem  10053  alephdom  10121  alephdom2  10127  cardaleph  10129  iscard3  10133  alephfp  10148  dfac12lem1  10184  dfac12lem2  10185  dfac12lem3  10186  cflim2  10303  cofsmo  10309  cfsmolem  10310  coftr  10313  cfcof  10314  fin67  10435  hsmexlem5  10470  zorn2lem6  10541  ttukeylem3  10551  ttukeylem5  10553  ttukeylem6  10554  ttukeylem7  10555  winainflem  10733  r1limwun  10776  r1wunlim  10777  tsksuc  10802  inar1  10815  gruina  10858  grur1a  10859  grur1  10860  nodmord  27698  noextendseq  27712  noextenddif  27713  nosupno  27748  nosupbday  27750  nosupres  27752  noinfno  27763  noinfbday  27765  noinfres  27767  noetasuplem4  27781  noetainflem4  27785  newbday  27940  dfrdg2  35796  ontgval  36432  ontgsucval  36433  onsuctopon  36435  onintopssconn  36441  onsuct0  36442  sucneqond  37366  onsucuni3  37368  aomclem4  43069  aomclem5  43070  onintunirab  43239  omlimcl2  43254  onelord  43263  oneltri  43270  ordeldifsucon  43272  ordeldif1o  43273  onsucss  43279  onsucf1olem  43283  onov0suclim  43287  oe0rif  43298  onsucwordi  43301  oege1  43319  cantnfresb  43337  omabs2  43345  ordsssucb  43348  tfsconcatlem  43349  tfsconcatfv2  43353  tfsconcatrn  43355  tfsconcatb0  43357  tfsconcat0b  43359  tfsconcatrev  43361  onsucunipr  43385  oaun3lem1  43387  oaun3lem2  43388  nadd1suc  43405  naddgeoa  43407  oaltom  43418  omltoe  43420  nlimsuc  43454  dfsucon  43536  minregex  43547  onfrALTlem3  44564  onfrALTlem2  44566  onfrALTlem3VD  44907  onfrALTlem2VD  44909  onsetreclem3  49226