Theorem eloni 6372

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

Syntax hints:   → wi 4   ∈ wcel 2143  Ord word 6361  Oncon0 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-v 3457  df-ss 3923  df-uni 4874  df-tr 5220  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-ord 6365  df-on 6366

This theorem is referenced by:  onelon  6387  onin  6394  ontri1  6397  onfr  6402  onelpss  6403  onsseleq  6404  onelss  6405  oneltri  6406  ontr1  6410  ontr2  6411  ordunidif  6413  on0eln0  6420  ordsssuc  6454  onsssuc  6455  onnbtwn  6459  onunel  6470  suc11  6472  onun2  6473  ontr  6474  onordi  6476  onssneli  6480  epweon  7775  epweonALT  7776  ordeleqon  7782  onss  7785  sucexeloni  7809  onpwsuc  7813  onpsssuc  7816  onsucmin  7818  ordunpr  7823  ordunisuc  7829  onsucuni2  7831  onuniorsuc  7834  ordunisuc2  7841  ordzsl  7842  onzsl  7843  nlimon  7848  tfinds  7857  tfindsg2  7859  nnord  7871  poseq  8155  soseq  8156  onfununi  8329  smo11  8352  smoord  8353  smoword  8354  smogt  8355  tfrlem1  8363  tfrlem9a  8374  tfrlem15  8380  tz7.44-2  8395  tz7.48lem  8429  ord3  8470  oe0m1  8507  oaordi  8532  oaord  8533  oacan  8534  oawordri  8536  oalimcl  8546  oaass  8547  omord2  8553  omcan  8555  omwordi  8557  omword1  8559  omword2  8560  om00  8561  omlimcl  8564  omass  8566  omeulem2  8569  omopth2  8570  oen0  8573  oeord  8575  oecan  8576  oewordi  8578  oeworde  8580  oelimcl  8587  oeeulem  8588  oeeui  8589  nnarcl  8603  nnawordi  8608  nnawordex  8624  oaabs2  8636  omabs  8638  omsmo  8645  cofonr  8661  naddcllem  8663  naddsuc2  8689  omxpenlem  9067  infensuc  9144  dif1enlem  9145  nndomog  9198  onomeneq  9199  ordiso  9479  ordtypelem2  9482  hartogslem1  9505  cantnflt  9642  cantnfp1lem3  9650  cantnfp1  9651  oemapso  9652  oemapvali  9654  cantnflem1d  9658  cantnflem1  9659  cantnf  9663  oemapwe  9664  cantnffval2  9665  cnfcom  9670  r111  9748  r1ordg  9751  rankonidlem  9801  bndrank  9814  r1pw  9818  r1pwALT  9819  rankbnd2  9842  tcrank  9857  cardprclem  9966  carduni  9968  cardmin2  9986  infxpenlem  9998  alephdom  10066  alephdom2  10072  cardaleph  10074  iscard3  10078  alephfp  10093  dfac12lem1  10128  dfac12lem2  10129  dfac12lem3  10130  cflim2  10248  cofsmo  10254  cfsmolem  10255  coftr  10258  cfcof  10259  fin67  10380  hsmexlem5  10415  zorn2lem6  10486  ttukeylem3  10496  ttukeylem5  10498  ttukeylem6  10499  ttukeylem7  10500  winainflem  10679  r1limwun  10722  r1wunlim  10723  tsksuc  10748  inar1  10761  gruina  10804  grur1a  10805  grur1  10806  nodmord  27798  noextendseq  27812  noextenddif  27813  nosupno  27848  nosupbday  27850  nosupres  27852  noinfno  27863  noinfbday  27865  noinfres  27867  noetasuplem4  27881  noetainflem4  27885  newbday  28076  oldfib  28551  fineqvnttrclse  35518  dfrdg2  36266  nmulprop  36663  ontgval  36923  ontgsucval  36924  onsuctopon  36926  onintopssconn  36932  onsuct0  36933  sucneqond  37992  onsucuni3  37994  aomclem4  43767  aomclem5  43768  onintunirab  43937  omlimcl2  43952  onelord  43961  ordeldifsucon  43969  ordeldif1o  43970  onsucss  43976  onsucf1olem  43980  onov0suclim  43984  oe0rif  43995  onsucwordi  43998  oege1  44016  cantnfresb  44034  omabs2  44042  ordsssucb  44045  tfsconcatlem  44046  tfsconcatfv2  44050  tfsconcatrn  44052  tfsconcatb0  44054  tfsconcat0b  44056  tfsconcatrev  44058  onsucunipr  44082  oaun3lem1  44084  oaun3lem2  44085  nadd1suc  44102  naddgeoa  44104  oaltom  44114  omltoe  44116  nlimsuc  44150  dfsucon  44232  minregex  44243  onfrALTlem3  45236  onfrALTlem2  45238  onfrALTlem3VD  45578  onfrALTlem2VD  45580  onsetreclem3  50468