Theorem eloni 6377

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Ord word 6366  Oncon0 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-v 3460  df-ss 3925  df-uni 4878  df-tr 5224  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-ord 6370  df-on 6371

This theorem is used by:  onelon  6392  onin  6399  ontri1  6402  onfr  6407  onelpss  6408  onsseleq  6409  onelss  6410  oneltri  6411  ontr1  6415  ontr2  6416  ordunidif  6418  on0eln0  6425  ordsssuc  6459  onsssuc  6460  onnbtwn  6464  onunel  6475  suc11  6477  onun2  6478  ontr  6479  onordi  6481  onssneli  6485  epweon  7783  epweonALT  7784  ordeleqon  7790  onss  7793  sucexeloni  7817  onpwsuc  7821  onpsssuc  7824  onsucmin  7826  ordunpr  7831  ordunisuc  7837  onsucuni2  7839  onuniorsuc  7842  ordunisuc2  7849  ordzsl  7850  onzsl  7851  nlimon  7856  tfinds  7865  tfindsg2  7867  nnord  7879  poseq  8163  soseq  8164  onfununi  8337  smo11  8360  smoord  8361  smoword  8362  smogt  8363  tfrlem1  8371  tfrlem9a  8382  tfrlem15  8388  tz7.44-2  8403  tz7.48lem  8437  ord3  8478  oe0m1  8515  oaordi  8540  oaord  8541  oacan  8542  oawordri  8544  oalimcl  8554  oaass  8555  omord2  8561  omcan  8563  omwordi  8565  omword1  8567  omword2  8568  om00  8569  omlimcl  8572  omass  8574  omeulem2  8577  omopth2  8578  oen0  8581  oeord  8583  oecan  8584  oewordi  8586  oeworde  8588  oelimcl  8595  oeeulem  8596  oeeui  8597  nnarcl  8611  nnawordi  8616  nnawordex  8632  oaabs2  8644  omabs  8646  omsmo  8653  cofonr  8669  naddcllem  8671  naddsuc2  8697  omxpenlem  9076  infensuc  9153  dif1enlem  9154  nndomog  9207  onomeneq  9208  ordiso  9488  ordtypelem2  9491  hartogslem1  9514  cantnflt  9651  cantnfp1lem3  9659  cantnfp1  9660  oemapso  9661  oemapvali  9663  cantnflem1d  9667  cantnflem1  9668  cantnf  9672  oemapwe  9673  cantnffval2  9674  cnfcom  9679  r111  9757  r1ordg  9760  rankonidlem  9810  bndrank  9823  r1pw  9827  r1pwALT  9828  rankbnd2  9851  tcrank  9866  cardprclem  9984  carduni  9986  cardmin2  10004  infxpenlem  10016  alephdom  10084  alephdom2  10090  cardaleph  10092  iscard3  10096  alephfp  10111  dfac12lem1  10146  dfac12lem2  10147  dfac12lem3  10148  cflim2  10265  cofsmo  10271  cfsmolem  10272  coftr  10275  cfcof  10276  fin67  10397  hsmexlem5  10432  zorn2lem6  10503  ttukeylem3  10513  ttukeylem5  10515  ttukeylem6  10516  ttukeylem7  10517  winainflem  10696  r1limwun  10739  r1wunlim  10740  tsksuc  10765  inar1  10778  gruina  10821  grur1a  10822  grur1  10823  nodmord  27854  noextendseq  27868  noextenddif  27869  nosupno  27904  nosupbday  27906  nosupres  27908  noinfno  27919  noinfbday  27921  noinfres  27923  noetasuplem4  27937  noetainflem4  27941  newbday  28132  oldfib  28607  fineqvnttrclse  35561  dfrdg2  36306  nmulprop  36703  ontgval  36983  ontgsucval  36984  onsuctopon  36986  onintopssconn  36992  onsuct0  36993  sucneqond  38052  onsucuni3  38054  aomclem4  43825  aomclem5  43826  onintunirab  43995  omlimcl2  44010  onelord  44019  ordeldifsucon  44027  ordeldif1o  44028  onsucss  44034  onsucf1olem  44038  onov0suclim  44042  oe0rif  44053  onsucwordi  44056  oege1  44074  cantnfresb  44092  omabs2  44100  ordsssucb  44103  tfsconcatlem  44104  tfsconcatfv2  44108  tfsconcatrn  44110  tfsconcatb0  44112  tfsconcat0b  44114  tfsconcatrev  44116  onsucunipr  44140  oaun3lem1  44142  oaun3lem2  44143  nadd1suc  44160  naddgeoa  44162  oaltom  44172  omltoe  44174  nlimsuc  44208  dfsucon  44290  minregex  44301  onfrALTlem3  45294  onfrALTlem2  45296  onfrALTlem3VD  45636  onfrALTlem2VD  45638  onsetreclem3  50526