Theorem eloni 6375

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 6364  Oncon0 6365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-tr 5267  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-ord 6368  df-on 6369

This theorem is referenced by:  onelon  6390  onin  6396  ontri1  6399  onfr  6404  onelpss  6405  onsseleq  6406  onelss  6407  ontr1  6411  ontr2  6412  ordunidif  6414  on0eln0  6421  ordsssuc  6454  onsssuc  6455  onnbtwn  6459  onunel  6470  suc11  6472  onun2  6473  ontr  6474  onordi  6476  onssneli  6481  epweon  7762  epweonALT  7763  ordeleqon  7769  onss  7772  sucexeloni  7797  ordsucOLD  7802  onpwsuc  7804  onpsssuc  7807  onsucmin  7809  ordunpr  7814  ordunisuc  7820  onsucuni2  7822  onuniorsuc  7825  ordunisuc2  7833  ordzsl  7834  onzsl  7835  nlimon  7840  tfinds  7849  tfindsg2  7851  nnord  7863  poseq  8144  soseq  8145  onfununi  8341  smo11  8364  smoord  8365  smoword  8366  smogt  8367  tfrlem1  8376  tfrlem9a  8386  tfrlem15  8392  tz7.44-2  8407  tz7.48lem  8441  ord3  8483  oe0m1  8521  oaordi  8546  oaord  8547  oacan  8548  oawordri  8550  oalimcl  8560  oaass  8561  omord2  8567  omcan  8569  omwordi  8571  omword1  8573  omword2  8574  om00  8575  omlimcl  8578  omass  8580  omeulem2  8583  omopth2  8584  oen0  8586  oeord  8588  oecan  8589  oewordi  8591  oeworde  8593  oelimcl  8600  oeeulem  8601  oeeui  8602  nnarcl  8616  nnawordi  8621  nnawordex  8637  oaabs2  8648  omabs  8650  omsmo  8657  cofonr  8673  naddcllem  8675  omxpenlem  9073  infensuc  9155  dif1enlem  9156  nndomog  9216  nndomogOLD  9226  onomeneq  9228  onomeneqOLD  9229  ordiso  9511  ordtypelem2  9514  hartogslem1  9537  cantnflt  9667  cantnfp1lem3  9675  cantnfp1  9676  oemapso  9677  oemapvali  9679  cantnflem1d  9683  cantnflem1  9684  cantnf  9688  oemapwe  9689  cantnffval2  9690  cnfcom  9695  r111  9770  r1ordg  9773  rankonidlem  9823  bndrank  9836  r1pw  9840  r1pwALT  9841  rankbnd2  9864  tcrank  9879  cardprclem  9974  carduni  9976  cardmin2  9994  infxpenlem  10008  alephdom  10076  alephdom2  10082  cardaleph  10084  iscard3  10088  alephfp  10103  dfac12lem1  10138  dfac12lem2  10139  dfac12lem3  10140  cflim2  10258  cofsmo  10264  cfsmolem  10265  coftr  10268  cfcof  10269  fin67  10390  hsmexlem5  10425  zorn2lem6  10496  ttukeylem3  10506  ttukeylem5  10508  ttukeylem6  10509  ttukeylem7  10510  winainflem  10688  r1limwun  10731  r1wunlim  10732  tsksuc  10757  inar1  10770  gruina  10813  grur1a  10814  grur1  10815  nodmord  27156  noextendseq  27170  noextenddif  27171  nosupno  27206  nosupbday  27208  nosupres  27210  noinfno  27221  noinfbday  27223  noinfres  27225  noetasuplem4  27239  noetainflem4  27243  newbday  27396  dfrdg2  34767  ontgval  35316  ontgsucval  35317  onsuctopon  35319  onintopssconn  35325  onsuct0  35326  sucneqond  36246  onsucuni3  36248  aomclem4  41799  aomclem5  41800  onintunirab  41976  omlimcl2  41991  onelord  42000  oneltri  42007  ordeldifsucon  42009  ordeldif1o  42010  onsucss  42016  onsucf1olem  42020  onov0suclim  42024  oe0rif  42035  onsucwordi  42038  oege1  42056  cantnfresb  42074  omabs2  42082  ordsssucb  42085  tfsconcatlem  42086  tfsconcatfv2  42090  tfsconcatrn  42092  tfsconcatb0  42094  tfsconcat0b  42096  tfsconcatrev  42098  onsucunipr  42122  oaun3lem1  42124  oaun3lem2  42125  nadd1suc  42142  naddsuc2  42143  naddgeoa  42145  oaltom  42156  omltoe  42158  nlimsuc  42192  dfsucon  42274  minregex  42285  onfrALTlem3  43305  onfrALTlem2  43307  onfrALTlem3VD  43648  onfrALTlem2VD  43650  onsetreclem3  47752