Theorem eloni 6327

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

Syntax hints:   → wi 4   ∈ wcel 2119  Ord word 6316  Oncon0 6317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-ss 3907  df-uni 4846  df-tr 5187  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-ord 6320  df-on 6321

This theorem is referenced by:  onelon  6342  onin  6348  ontri1  6351  onfr  6356  onelpss  6357  onsseleq  6358  onelss  6359  oneltri  6360  ontr1  6364  ontr2  6365  ordunidif  6367  on0eln0  6374  ordsssuc  6408  onsssuc  6409  onnbtwn  6413  onunel  6424  suc11  6426  onun2  6427  ontr  6428  onordi  6430  onssneli  6434  epweon  7725  epweonALT  7726  ordeleqon  7732  onss  7735  sucexeloni  7759  onpwsuc  7763  onpsssuc  7766  onsucmin  7768  ordunpr  7773  ordunisuc  7779  onsucuni2  7781  onuniorsuc  7784  ordunisuc2  7791  ordzsl  7792  onzsl  7793  nlimon  7798  tfinds  7807  tfindsg2  7809  nnord  7821  poseq  8105  soseq  8106  onfununi  8278  smo11  8301  smoord  8302  smoword  8303  smogt  8304  tfrlem1  8312  tfrlem9a  8322  tfrlem15  8328  tz7.44-2  8343  tz7.48lem  8377  ord3  8417  oe0m1  8453  oaordi  8478  oaord  8479  oacan  8480  oawordri  8482  oalimcl  8492  oaass  8493  omord2  8499  omcan  8501  omwordi  8503  omword1  8505  omword2  8506  om00  8507  omlimcl  8510  omass  8512  omeulem2  8515  omopth2  8516  oen0  8519  oeord  8521  oecan  8522  oewordi  8524  oeworde  8526  oelimcl  8533  oeeulem  8534  oeeui  8535  nnarcl  8549  nnawordi  8554  nnawordex  8570  oaabs2  8582  omabs  8584  omsmo  8591  cofonr  8607  naddcllem  8609  naddsuc2  8634  omxpenlem  9013  infensuc  9090  dif1enlem  9091  nndomog  9144  onomeneq  9145  ordiso  9428  ordtypelem2  9431  hartogslem1  9454  cantnflt  9591  cantnfp1lem3  9599  cantnfp1  9600  oemapso  9601  oemapvali  9603  cantnflem1d  9607  cantnflem1  9608  cantnf  9612  oemapwe  9613  cantnffval2  9614  cnfcom  9619  r111  9697  r1ordg  9700  rankonidlem  9750  bndrank  9763  r1pw  9767  r1pwALT  9768  rankbnd2  9791  tcrank  9806  cardprclem  9901  carduni  9903  cardmin2  9921  infxpenlem  9933  alephdom  10001  alephdom2  10007  cardaleph  10009  iscard3  10013  alephfp  10028  dfac12lem1  10064  dfac12lem2  10065  dfac12lem3  10066  cflim2  10183  cofsmo  10189  cfsmolem  10190  coftr  10193  cfcof  10194  fin67  10315  hsmexlem5  10350  zorn2lem6  10421  ttukeylem3  10431  ttukeylem5  10433  ttukeylem6  10434  ttukeylem7  10435  winainflem  10614  r1limwun  10657  r1wunlim  10658  tsksuc  10683  inar1  10696  gruina  10739  grur1a  10740  grur1  10741  nodmord  27642  noextendseq  27656  noextenddif  27657  nosupno  27692  nosupbday  27694  nosupres  27696  noinfno  27707  noinfbday  27709  noinfres  27711  noetasuplem4  27725  noetainflem4  27729  newbday  27919  oldfib  28394  fineqvnttrclse  35312  dfrdg2  36028  ontgval  36666  ontgsucval  36667  onsuctopon  36669  onintopssconn  36675  onsuct0  36676  sucneqond  37734  onsucuni3  37736  aomclem4  43509  aomclem5  43510  onintunirab  43679  omlimcl2  43694  onelord  43703  ordeldifsucon  43711  ordeldif1o  43712  onsucss  43718  onsucf1olem  43722  onov0suclim  43726  oe0rif  43737  onsucwordi  43740  oege1  43758  cantnfresb  43776  omabs2  43784  ordsssucb  43787  tfsconcatlem  43788  tfsconcatfv2  43792  tfsconcatrn  43794  tfsconcatb0  43796  tfsconcat0b  43798  tfsconcatrev  43800  onsucunipr  43824  oaun3lem1  43826  oaun3lem2  43827  nadd1suc  43844  naddgeoa  43846  oaltom  43856  omltoe  43858  nlimsuc  43892  dfsucon  43974  minregex  43985  onfrALTlem3  44995  onfrALTlem2  44997  onfrALTlem3VD  45337  onfrALTlem2VD  45339  onsetreclem3  50204