Theorem eloni 6333

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

Syntax hints:   → wi 4   ∈ wcel 2114  Ord word 6322  Oncon0 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-uni 4851  df-tr 5193  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-ord 6326  df-on 6327

This theorem is referenced by:  onelon  6348  onin  6354  ontri1  6357  onfr  6362  onelpss  6363  onsseleq  6364  onelss  6365  oneltri  6366  ontr1  6370  ontr2  6371  ordunidif  6373  on0eln0  6380  ordsssuc  6414  onsssuc  6415  onnbtwn  6419  onunel  6430  suc11  6432  onun2  6433  ontr  6434  onordi  6436  onssneli  6440  epweon  7729  epweonALT  7730  ordeleqon  7736  onss  7739  sucexeloni  7763  onpwsuc  7767  onpsssuc  7770  onsucmin  7772  ordunpr  7777  ordunisuc  7783  onsucuni2  7785  onuniorsuc  7788  ordunisuc2  7795  ordzsl  7796  onzsl  7797  nlimon  7802  tfinds  7811  tfindsg2  7813  nnord  7825  poseq  8108  soseq  8109  onfununi  8281  smo11  8304  smoord  8305  smoword  8306  smogt  8307  tfrlem1  8315  tfrlem9a  8325  tfrlem15  8331  tz7.44-2  8346  tz7.48lem  8380  ord3  8420  oe0m1  8456  oaordi  8481  oaord  8482  oacan  8483  oawordri  8485  oalimcl  8495  oaass  8496  omord2  8502  omcan  8504  omwordi  8506  omword1  8508  omword2  8509  om00  8510  omlimcl  8513  omass  8515  omeulem2  8518  omopth2  8519  oen0  8522  oeord  8524  oecan  8525  oewordi  8527  oeworde  8529  oelimcl  8536  oeeulem  8537  oeeui  8538  nnarcl  8552  nnawordi  8557  nnawordex  8573  oaabs2  8585  omabs  8587  omsmo  8594  cofonr  8610  naddcllem  8612  naddsuc2  8637  omxpenlem  9016  infensuc  9093  dif1enlem  9094  nndomog  9147  onomeneq  9148  ordiso  9431  ordtypelem2  9434  hartogslem1  9457  cantnflt  9593  cantnfp1lem3  9601  cantnfp1  9602  oemapso  9603  oemapvali  9605  cantnflem1d  9609  cantnflem1  9610  cantnf  9614  oemapwe  9615  cantnffval2  9616  cnfcom  9621  r111  9699  r1ordg  9702  rankonidlem  9752  bndrank  9765  r1pw  9769  r1pwALT  9770  rankbnd2  9793  tcrank  9808  cardprclem  9903  carduni  9905  cardmin2  9923  infxpenlem  9935  alephdom  10003  alephdom2  10009  cardaleph  10011  iscard3  10015  alephfp  10030  dfac12lem1  10066  dfac12lem2  10067  dfac12lem3  10068  cflim2  10185  cofsmo  10191  cfsmolem  10192  coftr  10195  cfcof  10196  fin67  10317  hsmexlem5  10352  zorn2lem6  10423  ttukeylem3  10433  ttukeylem5  10435  ttukeylem6  10436  ttukeylem7  10437  winainflem  10616  r1limwun  10659  r1wunlim  10660  tsksuc  10685  inar1  10698  gruina  10741  grur1a  10742  grur1  10743  nodmord  27617  noextendseq  27631  noextenddif  27632  nosupno  27667  nosupbday  27669  nosupres  27671  noinfno  27682  noinfbday  27684  noinfres  27686  noetasuplem4  27700  noetainflem4  27704  newbday  27894  oldfib  28369  fineqvnttrclse  35268  dfrdg2  35975  ontgval  36613  ontgsucval  36614  onsuctopon  36616  onintopssconn  36622  onsuct0  36623  sucneqond  37681  onsucuni3  37683  aomclem4  43485  aomclem5  43486  onintunirab  43655  omlimcl2  43670  onelord  43679  ordeldifsucon  43687  ordeldif1o  43688  onsucss  43694  onsucf1olem  43698  onov0suclim  43702  oe0rif  43713  onsucwordi  43716  oege1  43734  cantnfresb  43752  omabs2  43760  ordsssucb  43763  tfsconcatlem  43764  tfsconcatfv2  43768  tfsconcatrn  43770  tfsconcatb0  43772  tfsconcat0b  43774  tfsconcatrev  43776  onsucunipr  43800  oaun3lem1  43802  oaun3lem2  43803  nadd1suc  43820  naddgeoa  43822  oaltom  43832  omltoe  43834  nlimsuc  43868  dfsucon  43950  minregex  43961  onfrALTlem3  44971  onfrALTlem2  44973  onfrALTlem3VD  45313  onfrALTlem2VD  45315  onsetreclem3  50182