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  27397  dfrdg2  34798  ontgval  35364  ontgsucval  35365  onsuctopon  35367  onintopssconn  35373  onsuct0  35374  sucneqond  36294  onsucuni3  36296  aomclem4  41847  aomclem5  41848  onintunirab  42024  omlimcl2  42039  onelord  42048  oneltri  42055  ordeldifsucon  42057  ordeldif1o  42058  onsucss  42064  onsucf1olem  42068  onov0suclim  42072  oe0rif  42083  onsucwordi  42086  oege1  42104  cantnfresb  42122  omabs2  42130  ordsssucb  42133  tfsconcatlem  42134  tfsconcatfv2  42138  tfsconcatrn  42140  tfsconcatb0  42142  tfsconcat0b  42144  tfsconcatrev  42146  onsucunipr  42170  oaun3lem1  42172  oaun3lem2  42173  nadd1suc  42190  naddsuc2  42191  naddgeoa  42193  oaltom  42204  omltoe  42206  nlimsuc  42240  dfsucon  42322  minregex  42333  onfrALTlem3  43353  onfrALTlem2  43355  onfrALTlem3VD  43696  onfrALTlem2VD  43698  onsetreclem3  47800