Theorem eloni 6342

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6331  Oncon0 6332

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 3449  df-ss 3931  df-uni 4872  df-tr 5215  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-ord 6335  df-on 6336

This theorem is referenced by:  onelon  6357  onin  6363  ontri1  6366  onfr  6371  onelpss  6372  onsseleq  6373  onelss  6374  oneltri  6375  ontr1  6379  ontr2  6380  ordunidif  6382  on0eln0  6389  ordsssuc  6423  onsssuc  6424  onnbtwn  6428  onunel  6439  suc11  6441  onun2  6442  ontr  6443  onordi  6445  onssneli  6450  epweon  7751  epweonALT  7752  ordeleqon  7758  onss  7761  sucexeloni  7785  ordsucOLD  7789  onpwsuc  7791  onpsssuc  7794  onsucmin  7796  ordunpr  7801  ordunisuc  7807  onsucuni2  7809  onuniorsuc  7812  ordunisuc2  7820  ordzsl  7821  onzsl  7822  nlimon  7827  tfinds  7836  tfindsg2  7838  nnord  7850  poseq  8137  soseq  8138  onfununi  8310  smo11  8333  smoord  8334  smoword  8335  smogt  8336  tfrlem1  8344  tfrlem9a  8354  tfrlem15  8360  tz7.44-2  8375  tz7.48lem  8409  ord3  8449  oe0m1  8485  oaordi  8510  oaord  8511  oacan  8512  oawordri  8514  oalimcl  8524  oaass  8525  omord2  8531  omcan  8533  omwordi  8535  omword1  8537  omword2  8538  om00  8539  omlimcl  8542  omass  8544  omeulem2  8547  omopth2  8548  oen0  8550  oeord  8552  oecan  8553  oewordi  8555  oeworde  8557  oelimcl  8564  oeeulem  8565  oeeui  8566  nnarcl  8580  nnawordi  8585  nnawordex  8601  oaabs2  8613  omabs  8615  omsmo  8622  cofonr  8638  naddcllem  8640  naddsuc2  8665  omxpenlem  9042  infensuc  9119  dif1enlem  9120  nndomog  9177  onomeneq  9178  ordiso  9469  ordtypelem2  9472  hartogslem1  9495  cantnflt  9625  cantnfp1lem3  9633  cantnfp1  9634  oemapso  9635  oemapvali  9637  cantnflem1d  9641  cantnflem1  9642  cantnf  9646  oemapwe  9647  cantnffval2  9648  cnfcom  9653  r111  9728  r1ordg  9731  rankonidlem  9781  bndrank  9794  r1pw  9798  r1pwALT  9799  rankbnd2  9822  tcrank  9837  cardprclem  9932  carduni  9934  cardmin2  9952  infxpenlem  9966  alephdom  10034  alephdom2  10040  cardaleph  10042  iscard3  10046  alephfp  10061  dfac12lem1  10097  dfac12lem2  10098  dfac12lem3  10099  cflim2  10216  cofsmo  10222  cfsmolem  10223  coftr  10226  cfcof  10227  fin67  10348  hsmexlem5  10383  zorn2lem6  10454  ttukeylem3  10464  ttukeylem5  10466  ttukeylem6  10467  ttukeylem7  10468  winainflem  10646  r1limwun  10689  r1wunlim  10690  tsksuc  10715  inar1  10728  gruina  10771  grur1a  10772  grur1  10773  nodmord  27565  noextendseq  27579  noextenddif  27580  nosupno  27615  nosupbday  27617  nosupres  27619  noinfno  27630  noinfbday  27632  noinfres  27634  noetasuplem4  27648  noetainflem4  27652  newbday  27813  dfrdg2  35783  ontgval  36419  ontgsucval  36420  onsuctopon  36422  onintopssconn  36428  onsuct0  36429  sucneqond  37353  onsucuni3  37355  aomclem4  43046  aomclem5  43047  onintunirab  43216  omlimcl2  43231  onelord  43240  ordeldifsucon  43248  ordeldif1o  43249  onsucss  43255  onsucf1olem  43259  onov0suclim  43263  oe0rif  43274  onsucwordi  43277  oege1  43295  cantnfresb  43313  omabs2  43321  ordsssucb  43324  tfsconcatlem  43325  tfsconcatfv2  43329  tfsconcatrn  43331  tfsconcatb0  43333  tfsconcat0b  43335  tfsconcatrev  43337  onsucunipr  43361  oaun3lem1  43363  oaun3lem2  43364  nadd1suc  43381  naddgeoa  43383  oaltom  43394  omltoe  43396  nlimsuc  43430  dfsucon  43512  minregex  43523  onfrALTlem3  44534  onfrALTlem2  44536  onfrALTlem3VD  44876  onfrALTlem2VD  44878  onsetreclem3  49696