Theorem eloni 6352

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

Syntax hints:   → wi 4   ∈ wcel 2141  Ord word 6341  Oncon0 6342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-ss 3921  df-uni 4865  df-tr 5207  df-po 5553  df-so 5554  df-fr 5598  df-we 5600  df-ord 6345  df-on 6346

This theorem is referenced by:  onelon  6367  onin  6373  ontri1  6376  onfr  6381  onelpss  6382  onsseleq  6383  onelss  6384  oneltri  6385  ontr1  6389  ontr2  6390  ordunidif  6392  on0eln0  6399  ordsssuc  6433  onsssuc  6434  onnbtwn  6438  onunel  6449  suc11  6451  onun2  6452  ontr  6453  onordi  6455  onssneli  6459  epweon  7754  epweonALT  7755  ordeleqon  7761  onss  7764  sucexeloni  7788  onpwsuc  7792  onpsssuc  7795  onsucmin  7797  ordunpr  7802  ordunisuc  7808  onsucuni2  7810  onuniorsuc  7813  ordunisuc2  7820  ordzsl  7821  onzsl  7822  nlimon  7827  tfinds  7836  tfindsg2  7838  nnord  7850  poseq  8133  soseq  8134  onfununi  8307  smo11  8330  smoord  8331  smoword  8332  smogt  8333  tfrlem1  8341  tfrlem9a  8352  tfrlem15  8358  tz7.44-2  8373  tz7.48lem  8407  ord3  8448  oe0m1  8485  oaordi  8510  oaord  8511  oacan  8512  oawordri  8514  oalimcl  8524  oaass  8525  omord2  8531  omcan  8533  omwordi  8535  omword1  8537  omword2  8538  om00  8539  omlimcl  8542  omass  8544  omeulem2  8547  omopth2  8548  oen0  8551  oeord  8553  oecan  8554  oewordi  8556  oeworde  8558  oelimcl  8565  oeeulem  8566  oeeui  8567  nnarcl  8581  nnawordi  8586  nnawordex  8602  oaabs2  8614  omabs  8616  omsmo  8623  cofonr  8639  naddcllem  8641  naddsuc2  8667  omxpenlem  9046  infensuc  9123  dif1enlem  9124  nndomog  9177  onomeneq  9178  ordiso  9461  ordtypelem2  9464  hartogslem1  9487  cantnflt  9624  cantnfp1lem3  9632  cantnfp1  9633  oemapso  9634  oemapvali  9636  cantnflem1d  9640  cantnflem1  9641  cantnf  9645  oemapwe  9646  cantnffval2  9647  cnfcom  9652  r111  9730  r1ordg  9733  rankonidlem  9783  bndrank  9796  r1pw  9800  r1pwALT  9801  rankbnd2  9824  tcrank  9839  cardprclem  9934  carduni  9936  cardmin2  9954  infxpenlem  9966  alephdom  10034  alephdom2  10040  cardaleph  10042  iscard3  10046  alephfp  10061  dfac12lem1  10097  dfac12lem2  10098  dfac12lem3  10099  cflim2  10217  cofsmo  10223  cfsmolem  10224  coftr  10227  cfcof  10228  fin67  10349  hsmexlem5  10384  zorn2lem6  10455  ttukeylem3  10465  ttukeylem5  10467  ttukeylem6  10468  ttukeylem7  10469  winainflem  10648  r1limwun  10691  r1wunlim  10692  tsksuc  10717  inar1  10730  gruina  10773  grur1a  10774  grur1  10775  nodmord  27694  noextendseq  27708  noextenddif  27709  nosupno  27744  nosupbday  27746  nosupres  27748  noinfno  27759  noinfbday  27761  noinfres  27763  noetasuplem4  27777  noetainflem4  27781  newbday  27972  oldfib  28447  fineqvnttrclse  35384  dfrdg2  36107  nmulprop  36504  ontgval  36755  ontgsucval  36756  onsuctopon  36758  onintopssconn  36764  onsuct0  36765  sucneqond  37823  onsucuni3  37825  aomclem4  43598  aomclem5  43599  onintunirab  43768  omlimcl2  43783  onelord  43792  ordeldifsucon  43800  ordeldif1o  43801  onsucss  43807  onsucf1olem  43811  onov0suclim  43815  oe0rif  43826  onsucwordi  43829  oege1  43847  cantnfresb  43865  omabs2  43873  ordsssucb  43876  tfsconcatlem  43877  tfsconcatfv2  43881  tfsconcatrn  43883  tfsconcatb0  43885  tfsconcat0b  43887  tfsconcatrev  43889  onsucunipr  43913  oaun3lem1  43915  oaun3lem2  43916  nadd1suc  43933  naddgeoa  43935  oaltom  43945  omltoe  43947  nlimsuc  43981  dfsucon  44063  minregex  44074  onfrALTlem3  45084  onfrALTlem2  45086  onfrALTlem3VD  45426  onfrALTlem2VD  45428  onsetreclem3  50292