Theorem eloni 6345

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

Syntax hints:   → wi 4   ∈ wcel 2109  Ord word 6334  Oncon0 6335

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-uni 4875  df-tr 5218  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-ord 6338  df-on 6339

This theorem is referenced by:  onelon  6360  onin  6366  ontri1  6369  onfr  6374  onelpss  6375  onsseleq  6376  onelss  6377  oneltri  6378  ontr1  6382  ontr2  6383  ordunidif  6385  on0eln0  6392  ordsssuc  6426  onsssuc  6427  onnbtwn  6431  onunel  6442  suc11  6444  onun2  6445  ontr  6446  onordi  6448  onssneli  6453  epweon  7754  epweonALT  7755  ordeleqon  7761  onss  7764  sucexeloni  7788  ordsucOLD  7792  onpwsuc  7794  onpsssuc  7797  onsucmin  7799  ordunpr  7804  ordunisuc  7810  onsucuni2  7812  onuniorsuc  7815  ordunisuc2  7823  ordzsl  7824  onzsl  7825  nlimon  7830  tfinds  7839  tfindsg2  7841  nnord  7853  poseq  8140  soseq  8141  onfununi  8313  smo11  8336  smoord  8337  smoword  8338  smogt  8339  tfrlem1  8347  tfrlem9a  8357  tfrlem15  8363  tz7.44-2  8378  tz7.48lem  8412  ord3  8452  oe0m1  8488  oaordi  8513  oaord  8514  oacan  8515  oawordri  8517  oalimcl  8527  oaass  8528  omord2  8534  omcan  8536  omwordi  8538  omword1  8540  omword2  8541  om00  8542  omlimcl  8545  omass  8547  omeulem2  8550  omopth2  8551  oen0  8553  oeord  8555  oecan  8556  oewordi  8558  oeworde  8560  oelimcl  8567  oeeulem  8568  oeeui  8569  nnarcl  8583  nnawordi  8588  nnawordex  8604  oaabs2  8616  omabs  8618  omsmo  8625  cofonr  8641  naddcllem  8643  naddsuc2  8668  omxpenlem  9047  infensuc  9125  dif1enlem  9126  nndomog  9183  onomeneq  9184  ordiso  9476  ordtypelem2  9479  hartogslem1  9502  cantnflt  9632  cantnfp1lem3  9640  cantnfp1  9641  oemapso  9642  oemapvali  9644  cantnflem1d  9648  cantnflem1  9649  cantnf  9653  oemapwe  9654  cantnffval2  9655  cnfcom  9660  r111  9735  r1ordg  9738  rankonidlem  9788  bndrank  9801  r1pw  9805  r1pwALT  9806  rankbnd2  9829  tcrank  9844  cardprclem  9939  carduni  9941  cardmin2  9959  infxpenlem  9973  alephdom  10041  alephdom2  10047  cardaleph  10049  iscard3  10053  alephfp  10068  dfac12lem1  10104  dfac12lem2  10105  dfac12lem3  10106  cflim2  10223  cofsmo  10229  cfsmolem  10230  coftr  10233  cfcof  10234  fin67  10355  hsmexlem5  10390  zorn2lem6  10461  ttukeylem3  10471  ttukeylem5  10473  ttukeylem6  10474  ttukeylem7  10475  winainflem  10653  r1limwun  10696  r1wunlim  10697  tsksuc  10722  inar1  10735  gruina  10778  grur1a  10779  grur1  10780  nodmord  27572  noextendseq  27586  noextenddif  27587  nosupno  27622  nosupbday  27624  nosupres  27626  noinfno  27637  noinfbday  27639  noinfres  27641  noetasuplem4  27655  noetainflem4  27659  newbday  27820  dfrdg2  35790  ontgval  36426  ontgsucval  36427  onsuctopon  36429  onintopssconn  36435  onsuct0  36436  sucneqond  37360  onsucuni3  37362  aomclem4  43053  aomclem5  43054  onintunirab  43223  omlimcl2  43238  onelord  43247  ordeldifsucon  43255  ordeldif1o  43256  onsucss  43262  onsucf1olem  43266  onov0suclim  43270  oe0rif  43281  onsucwordi  43284  oege1  43302  cantnfresb  43320  omabs2  43328  ordsssucb  43331  tfsconcatlem  43332  tfsconcatfv2  43336  tfsconcatrn  43338  tfsconcatb0  43340  tfsconcat0b  43342  tfsconcatrev  43344  onsucunipr  43368  oaun3lem1  43370  oaun3lem2  43371  nadd1suc  43388  naddgeoa  43390  oaltom  43401  omltoe  43403  nlimsuc  43437  dfsucon  43519  minregex  43530  onfrALTlem3  44541  onfrALTlem2  44543  onfrALTlem3VD  44883  onfrALTlem2VD  44885  onsetreclem3  49700