Theorem eloni 6359

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 6348  Oncon0 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-v 3459  df-ss 3941  df-uni 4881  df-tr 5227  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6352  df-on 6353

This theorem is referenced by:  onelon  6374  onin  6380  ontri1  6383  onfr  6388  onelpss  6389  onsseleq  6390  onelss  6391  oneltri  6392  ontr1  6396  ontr2  6397  ordunidif  6399  on0eln0  6406  ordsssuc  6439  onsssuc  6440  onnbtwn  6444  onunel  6455  suc11  6457  onun2  6458  ontr  6459  onordi  6461  onssneli  6466  epweon  7763  epweonALT  7764  ordeleqon  7770  onss  7773  sucexeloni  7797  ordsucOLD  7802  onpwsuc  7804  onpsssuc  7807  onsucmin  7809  ordunpr  7814  ordunisuc  7820  onsucuni2  7822  onuniorsuc  7825  ordunisuc2  7833  ordzsl  7834  onzsl  7835  nlimon  7840  tfinds  7849  tfindsg2  7851  nnord  7863  poseq  8151  soseq  8152  onfununi  8349  smo11  8372  smoord  8373  smoword  8374  smogt  8375  tfrlem1  8384  tfrlem9a  8394  tfrlem15  8400  tz7.44-2  8415  tz7.48lem  8449  ord3  8491  oe0m1  8527  oaordi  8552  oaord  8553  oacan  8554  oawordri  8556  oalimcl  8566  oaass  8567  omord2  8573  omcan  8575  omwordi  8577  omword1  8579  omword2  8580  om00  8581  omlimcl  8584  omass  8586  omeulem2  8589  omopth2  8590  oen0  8592  oeord  8594  oecan  8595  oewordi  8597  oeworde  8599  oelimcl  8606  oeeulem  8607  oeeui  8608  nnarcl  8622  nnawordi  8627  nnawordex  8643  oaabs2  8655  omabs  8657  omsmo  8664  cofonr  8680  naddcllem  8682  naddsuc2  8707  omxpenlem  9081  infensuc  9163  dif1enlem  9164  nndomog  9221  nndomogOLD  9229  onomeneq  9231  onomeneqOLD  9232  ordiso  9522  ordtypelem2  9525  hartogslem1  9548  cantnflt  9678  cantnfp1lem3  9686  cantnfp1  9687  oemapso  9688  oemapvali  9690  cantnflem1d  9694  cantnflem1  9695  cantnf  9699  oemapwe  9700  cantnffval2  9701  cnfcom  9706  r111  9781  r1ordg  9784  rankonidlem  9834  bndrank  9847  r1pw  9851  r1pwALT  9852  rankbnd2  9875  tcrank  9890  cardprclem  9985  carduni  9987  cardmin2  10005  infxpenlem  10019  alephdom  10087  alephdom2  10093  cardaleph  10095  iscard3  10099  alephfp  10114  dfac12lem1  10150  dfac12lem2  10151  dfac12lem3  10152  cflim2  10269  cofsmo  10275  cfsmolem  10276  coftr  10279  cfcof  10280  fin67  10401  hsmexlem5  10436  zorn2lem6  10507  ttukeylem3  10517  ttukeylem5  10519  ttukeylem6  10520  ttukeylem7  10521  winainflem  10699  r1limwun  10742  r1wunlim  10743  tsksuc  10768  inar1  10781  gruina  10824  grur1a  10825  grur1  10826  nodmord  27601  noextendseq  27615  noextenddif  27616  nosupno  27651  nosupbday  27653  nosupres  27655  noinfno  27666  noinfbday  27668  noinfres  27670  noetasuplem4  27684  noetainflem4  27688  newbday  27843  dfrdg2  35734  ontgval  36370  ontgsucval  36371  onsuctopon  36373  onintopssconn  36379  onsuct0  36380  sucneqond  37304  onsucuni3  37306  aomclem4  43006  aomclem5  43007  onintunirab  43176  omlimcl2  43191  onelord  43200  ordeldifsucon  43208  ordeldif1o  43209  onsucss  43215  onsucf1olem  43219  onov0suclim  43223  oe0rif  43234  onsucwordi  43237  oege1  43255  cantnfresb  43273  omabs2  43281  ordsssucb  43284  tfsconcatlem  43285  tfsconcatfv2  43289  tfsconcatrn  43291  tfsconcatb0  43293  tfsconcat0b  43295  tfsconcatrev  43297  onsucunipr  43321  oaun3lem1  43323  oaun3lem2  43324  nadd1suc  43341  naddgeoa  43343  oaltom  43354  omltoe  43356  nlimsuc  43390  dfsucon  43472  minregex  43483  onfrALTlem3  44495  onfrALTlem2  44497  onfrALTlem3VD  44838  onfrALTlem2VD  44840  onsetreclem3  49291