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 267	1 ⊢ (𝐴 ∈ On → Ord 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2113  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-uni 4864  df-tr 5206  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  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  7720  epweonALT  7721  ordeleqon  7727  onss  7730  sucexeloni  7754  onpwsuc  7758  onpsssuc  7761  onsucmin  7763  ordunpr  7768  ordunisuc  7774  onsucuni2  7776  onuniorsuc  7779  ordunisuc2  7786  ordzsl  7787  onzsl  7788  nlimon  7793  tfinds  7802  tfindsg2  7804  nnord  7816  poseq  8100  soseq  8101  onfununi  8273  smo11  8296  smoord  8297  smoword  8298  smogt  8299  tfrlem1  8307  tfrlem9a  8317  tfrlem15  8323  tz7.44-2  8338  tz7.48lem  8372  ord3  8412  oe0m1  8448  oaordi  8473  oaord  8474  oacan  8475  oawordri  8477  oalimcl  8487  oaass  8488  omord2  8494  omcan  8496  omwordi  8498  omword1  8500  omword2  8501  om00  8502  omlimcl  8505  omass  8507  omeulem2  8510  omopth2  8511  oen0  8514  oeord  8516  oecan  8517  oewordi  8519  oeworde  8521  oelimcl  8528  oeeulem  8529  oeeui  8530  nnarcl  8544  nnawordi  8549  nnawordex  8565  oaabs2  8577  omabs  8579  omsmo  8586  cofonr  8602  naddcllem  8604  naddsuc2  8629  omxpenlem  9006  infensuc  9083  dif1enlem  9084  nndomog  9137  onomeneq  9138  ordiso  9421  ordtypelem2  9424  hartogslem1  9447  cantnflt  9581  cantnfp1lem3  9589  cantnfp1  9590  oemapso  9591  oemapvali  9593  cantnflem1d  9597  cantnflem1  9598  cantnf  9602  oemapwe  9603  cantnffval2  9604  cnfcom  9609  r111  9687  r1ordg  9690  rankonidlem  9740  bndrank  9753  r1pw  9757  r1pwALT  9758  rankbnd2  9781  tcrank  9796  cardprclem  9891  carduni  9893  cardmin2  9911  infxpenlem  9923  alephdom  9991  alephdom2  9997  cardaleph  9999  iscard3  10003  alephfp  10018  dfac12lem1  10054  dfac12lem2  10055  dfac12lem3  10056  cflim2  10173  cofsmo  10179  cfsmolem  10180  coftr  10183  cfcof  10184  fin67  10305  hsmexlem5  10340  zorn2lem6  10411  ttukeylem3  10421  ttukeylem5  10423  ttukeylem6  10424  ttukeylem7  10425  winainflem  10604  r1limwun  10647  r1wunlim  10648  tsksuc  10673  inar1  10686  gruina  10729  grur1a  10730  grur1  10731  nodmord  27621  noextendseq  27635  noextenddif  27636  nosupno  27671  nosupbday  27673  nosupres  27675  noinfno  27686  noinfbday  27688  noinfres  27690  noetasuplem4  27704  noetainflem4  27708  newbday  27898  oldfib  28373  fineqvnttrclse  35280  dfrdg2  35987  ontgval  36625  ontgsucval  36626  onsuctopon  36628  onintopssconn  36634  onsuct0  36635  sucneqond  37566  onsucuni3  37568  aomclem4  43295  aomclem5  43296  onintunirab  43465  omlimcl2  43480  onelord  43489  ordeldifsucon  43497  ordeldif1o  43498  onsucss  43504  onsucf1olem  43508  onov0suclim  43512  oe0rif  43523  onsucwordi  43526  oege1  43544  cantnfresb  43562  omabs2  43570  ordsssucb  43573  tfsconcatlem  43574  tfsconcatfv2  43578  tfsconcatrn  43580  tfsconcatb0  43582  tfsconcat0b  43584  tfsconcatrev  43586  onsucunipr  43610  oaun3lem1  43612  oaun3lem2  43613  nadd1suc  43630  naddgeoa  43632  oaltom  43642  omltoe  43644  nlimsuc  43678  dfsucon  43760  minregex  43771  onfrALTlem3  44781  onfrALTlem2  44783  onfrALTlem3VD  45123  onfrALTlem2VD  45125  onsetreclem3  49948