Theorem eloni 6321

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

Syntax hints:   → wi 4   ∈ wcel 2113  Ord word 6310  Oncon0 6311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-ss 3915  df-uni 4859  df-tr 5201  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6314  df-on 6315

This theorem is referenced by:  onelon  6336  onin  6342  ontri1  6345  onfr  6350  onelpss  6351  onsseleq  6352  onelss  6353  oneltri  6354  ontr1  6358  ontr2  6359  ordunidif  6361  on0eln0  6368  ordsssuc  6402  onsssuc  6403  onnbtwn  6407  onunel  6418  suc11  6420  onun2  6421  ontr  6422  onordi  6424  onssneli  6428  epweon  7714  epweonALT  7715  ordeleqon  7721  onss  7724  sucexeloni  7748  onpwsuc  7752  onpsssuc  7755  onsucmin  7757  ordunpr  7762  ordunisuc  7768  onsucuni2  7770  onuniorsuc  7773  ordunisuc2  7780  ordzsl  7781  onzsl  7782  nlimon  7787  tfinds  7796  tfindsg2  7798  nnord  7810  poseq  8094  soseq  8095  onfununi  8267  smo11  8290  smoord  8291  smoword  8292  smogt  8293  tfrlem1  8301  tfrlem9a  8311  tfrlem15  8317  tz7.44-2  8332  tz7.48lem  8366  ord3  8406  oe0m1  8442  oaordi  8467  oaord  8468  oacan  8469  oawordri  8471  oalimcl  8481  oaass  8482  omord2  8488  omcan  8490  omwordi  8492  omword1  8494  omword2  8495  om00  8496  omlimcl  8499  omass  8501  omeulem2  8504  omopth2  8505  oen0  8507  oeord  8509  oecan  8510  oewordi  8512  oeworde  8514  oelimcl  8521  oeeulem  8522  oeeui  8523  nnarcl  8537  nnawordi  8542  nnawordex  8558  oaabs2  8570  omabs  8572  omsmo  8579  cofonr  8595  naddcllem  8597  naddsuc2  8622  omxpenlem  8998  infensuc  9075  dif1enlem  9076  nndomog  9129  onomeneq  9130  ordiso  9409  ordtypelem2  9412  hartogslem1  9435  cantnflt  9569  cantnfp1lem3  9577  cantnfp1  9578  oemapso  9579  oemapvali  9581  cantnflem1d  9585  cantnflem1  9586  cantnf  9590  oemapwe  9591  cantnffval2  9592  cnfcom  9597  r111  9675  r1ordg  9678  rankonidlem  9728  bndrank  9741  r1pw  9745  r1pwALT  9746  rankbnd2  9769  tcrank  9784  cardprclem  9879  carduni  9881  cardmin2  9899  infxpenlem  9911  alephdom  9979  alephdom2  9985  cardaleph  9987  iscard3  9991  alephfp  10006  dfac12lem1  10042  dfac12lem2  10043  dfac12lem3  10044  cflim2  10161  cofsmo  10167  cfsmolem  10168  coftr  10171  cfcof  10172  fin67  10293  hsmexlem5  10328  zorn2lem6  10399  ttukeylem3  10409  ttukeylem5  10411  ttukeylem6  10412  ttukeylem7  10413  winainflem  10591  r1limwun  10634  r1wunlim  10635  tsksuc  10660  inar1  10673  gruina  10716  grur1a  10717  grur1  10718  nodmord  27593  noextendseq  27607  noextenddif  27608  nosupno  27643  nosupbday  27645  nosupres  27647  noinfno  27658  noinfbday  27660  noinfres  27662  noetasuplem4  27676  noetainflem4  27680  newbday  27848  fineqvnttrclse  35165  dfrdg2  35858  ontgval  36496  ontgsucval  36497  onsuctopon  36499  onintopssconn  36505  onsuct0  36506  sucneqond  37430  onsucuni3  37432  aomclem4  43174  aomclem5  43175  onintunirab  43344  omlimcl2  43359  onelord  43368  ordeldifsucon  43376  ordeldif1o  43377  onsucss  43383  onsucf1olem  43387  onov0suclim  43391  oe0rif  43402  onsucwordi  43405  oege1  43423  cantnfresb  43441  omabs2  43449  ordsssucb  43452  tfsconcatlem  43453  tfsconcatfv2  43457  tfsconcatrn  43459  tfsconcatb0  43461  tfsconcat0b  43463  tfsconcatrev  43465  onsucunipr  43489  oaun3lem1  43491  oaun3lem2  43492  nadd1suc  43509  naddgeoa  43511  oaltom  43522  omltoe  43524  nlimsuc  43558  dfsucon  43640  minregex  43651  onfrALTlem3  44661  onfrALTlem2  44663  onfrALTlem3VD  45003  onfrALTlem2VD  45005  onsetreclem3  49832