Theorem eloni 6362

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

Syntax hints:   → wi 4   ∈ wcel 2108  Ord word 6351  Oncon0 6352

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-uni 4884  df-tr 5230  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-ord 6355  df-on 6356

This theorem is referenced by:  onelon  6377  onin  6383  ontri1  6386  onfr  6391  onelpss  6392  onsseleq  6393  onelss  6394  oneltri  6395  ontr1  6399  ontr2  6400  ordunidif  6402  on0eln0  6409  ordsssuc  6442  onsssuc  6443  onnbtwn  6447  onunel  6458  suc11  6460  onun2  6461  ontr  6462  onordi  6464  onssneli  6469  epweon  7767  epweonALT  7768  ordeleqon  7774  onss  7777  sucexeloni  7801  ordsucOLD  7806  onpwsuc  7808  onpsssuc  7811  onsucmin  7813  ordunpr  7818  ordunisuc  7824  onsucuni2  7826  onuniorsuc  7829  ordunisuc2  7837  ordzsl  7838  onzsl  7839  nlimon  7844  tfinds  7853  tfindsg2  7855  nnord  7867  poseq  8155  soseq  8156  onfununi  8353  smo11  8376  smoord  8377  smoword  8378  smogt  8379  tfrlem1  8388  tfrlem9a  8398  tfrlem15  8404  tz7.44-2  8419  tz7.48lem  8453  ord3  8495  oe0m1  8531  oaordi  8556  oaord  8557  oacan  8558  oawordri  8560  oalimcl  8570  oaass  8571  omord2  8577  omcan  8579  omwordi  8581  omword1  8583  omword2  8584  om00  8585  omlimcl  8588  omass  8590  omeulem2  8593  omopth2  8594  oen0  8596  oeord  8598  oecan  8599  oewordi  8601  oeworde  8603  oelimcl  8610  oeeulem  8611  oeeui  8612  nnarcl  8626  nnawordi  8631  nnawordex  8647  oaabs2  8659  omabs  8661  omsmo  8668  cofonr  8684  naddcllem  8686  naddsuc2  8711  omxpenlem  9085  infensuc  9167  dif1enlem  9168  nndomog  9225  nndomogOLD  9233  onomeneq  9235  onomeneqOLD  9236  ordiso  9528  ordtypelem2  9531  hartogslem1  9554  cantnflt  9684  cantnfp1lem3  9692  cantnfp1  9693  oemapso  9694  oemapvali  9696  cantnflem1d  9700  cantnflem1  9701  cantnf  9705  oemapwe  9706  cantnffval2  9707  cnfcom  9712  r111  9787  r1ordg  9790  rankonidlem  9840  bndrank  9853  r1pw  9857  r1pwALT  9858  rankbnd2  9881  tcrank  9896  cardprclem  9991  carduni  9993  cardmin2  10011  infxpenlem  10025  alephdom  10093  alephdom2  10099  cardaleph  10101  iscard3  10105  alephfp  10120  dfac12lem1  10156  dfac12lem2  10157  dfac12lem3  10158  cflim2  10275  cofsmo  10281  cfsmolem  10282  coftr  10285  cfcof  10286  fin67  10407  hsmexlem5  10442  zorn2lem6  10513  ttukeylem3  10523  ttukeylem5  10525  ttukeylem6  10526  ttukeylem7  10527  winainflem  10705  r1limwun  10748  r1wunlim  10749  tsksuc  10774  inar1  10787  gruina  10830  grur1a  10831  grur1  10832  nodmord  27615  noextendseq  27629  noextenddif  27630  nosupno  27665  nosupbday  27667  nosupres  27669  noinfno  27680  noinfbday  27682  noinfres  27684  noetasuplem4  27698  noetainflem4  27702  newbday  27857  dfrdg2  35759  ontgval  36395  ontgsucval  36396  onsuctopon  36398  onintopssconn  36404  onsuct0  36405  sucneqond  37329  onsucuni3  37331  aomclem4  43028  aomclem5  43029  onintunirab  43198  omlimcl2  43213  onelord  43222  ordeldifsucon  43230  ordeldif1o  43231  onsucss  43237  onsucf1olem  43241  onov0suclim  43245  oe0rif  43256  onsucwordi  43259  oege1  43277  cantnfresb  43295  omabs2  43303  ordsssucb  43306  tfsconcatlem  43307  tfsconcatfv2  43311  tfsconcatrn  43313  tfsconcatb0  43315  tfsconcat0b  43317  tfsconcatrev  43319  onsucunipr  43343  oaun3lem1  43345  oaun3lem2  43346  nadd1suc  43363  naddgeoa  43365  oaltom  43376  omltoe  43378  nlimsuc  43412  dfsucon  43494  minregex  43505  onfrALTlem3  44517  onfrALTlem2  44519  onfrALTlem3VD  44859  onfrALTlem2VD  44861  onsetreclem3  49519