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 2109  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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-ss 3922  df-uni 4862  df-tr 5203  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  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  7715  epweonALT  7716  ordeleqon  7722  onss  7725  sucexeloni  7749  ordsucOLD  7753  onpwsuc  7755  onpsssuc  7758  onsucmin  7760  ordunpr  7765  ordunisuc  7771  onsucuni2  7773  onuniorsuc  7776  ordunisuc2  7784  ordzsl  7785  onzsl  7786  nlimon  7791  tfinds  7800  tfindsg2  7802  nnord  7814  poseq  8098  soseq  8099  onfununi  8271  smo11  8294  smoord  8295  smoword  8296  smogt  8297  tfrlem1  8305  tfrlem9a  8315  tfrlem15  8321  tz7.44-2  8336  tz7.48lem  8370  ord3  8410  oe0m1  8446  oaordi  8471  oaord  8472  oacan  8473  oawordri  8475  oalimcl  8485  oaass  8486  omord2  8492  omcan  8494  omwordi  8496  omword1  8498  omword2  8499  om00  8500  omlimcl  8503  omass  8505  omeulem2  8508  omopth2  8509  oen0  8511  oeord  8513  oecan  8514  oewordi  8516  oeworde  8518  oelimcl  8525  oeeulem  8526  oeeui  8527  nnarcl  8541  nnawordi  8546  nnawordex  8562  oaabs2  8574  omabs  8576  omsmo  8583  cofonr  8599  naddcllem  8601  naddsuc2  8626  omxpenlem  9002  infensuc  9079  dif1enlem  9080  nndomog  9137  onomeneq  9138  ordiso  9427  ordtypelem2  9430  hartogslem1  9453  cantnflt  9587  cantnfp1lem3  9595  cantnfp1  9596  oemapso  9597  oemapvali  9599  cantnflem1d  9603  cantnflem1  9604  cantnf  9608  oemapwe  9609  cantnffval2  9610  cnfcom  9615  r111  9690  r1ordg  9693  rankonidlem  9743  bndrank  9756  r1pw  9760  r1pwALT  9761  rankbnd2  9784  tcrank  9799  cardprclem  9894  carduni  9896  cardmin2  9914  infxpenlem  9926  alephdom  9994  alephdom2  10000  cardaleph  10002  iscard3  10006  alephfp  10021  dfac12lem1  10057  dfac12lem2  10058  dfac12lem3  10059  cflim2  10176  cofsmo  10182  cfsmolem  10183  coftr  10186  cfcof  10187  fin67  10308  hsmexlem5  10343  zorn2lem6  10414  ttukeylem3  10424  ttukeylem5  10426  ttukeylem6  10427  ttukeylem7  10428  winainflem  10606  r1limwun  10649  r1wunlim  10650  tsksuc  10675  inar1  10688  gruina  10731  grur1a  10732  grur1  10733  nodmord  27581  noextendseq  27595  noextenddif  27596  nosupno  27631  nosupbday  27633  nosupres  27635  noinfno  27646  noinfbday  27648  noinfres  27650  noetasuplem4  27664  noetainflem4  27668  newbday  27834  dfrdg2  35768  ontgval  36404  ontgsucval  36405  onsuctopon  36407  onintopssconn  36413  onsuct0  36414  sucneqond  37338  onsucuni3  37340  aomclem4  43030  aomclem5  43031  onintunirab  43200  omlimcl2  43215  onelord  43224  ordeldifsucon  43232  ordeldif1o  43233  onsucss  43239  onsucf1olem  43243  onov0suclim  43247  oe0rif  43258  onsucwordi  43261  oege1  43279  cantnfresb  43297  omabs2  43305  ordsssucb  43308  tfsconcatlem  43309  tfsconcatfv2  43313  tfsconcatrn  43315  tfsconcatb0  43317  tfsconcat0b  43319  tfsconcatrev  43321  onsucunipr  43345  oaun3lem1  43347  oaun3lem2  43348  nadd1suc  43365  naddgeoa  43367  oaltom  43378  omltoe  43380  nlimsuc  43414  dfsucon  43496  minregex  43507  onfrALTlem3  44518  onfrALTlem2  44520  onfrALTlem3VD  44860  onfrALTlem2VD  44862  onsetreclem3  49693