Theorem eloni 6371

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Ord word 6360  Oncon0 6361

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-ss 3919  df-uni 4871  df-tr 5217  df-po 5567  df-so 5568  df-fr 5612  df-we 5614  df-ord 6364  df-on 6365

This theorem is used by:  onelon  6386  onin  6393  ontri1  6396  onfr  6401  onelpss  6402  onsseleq  6403  onelss  6404  oneltri  6405  ontr1  6409  ontr2  6410  ordunidif  6412  on0eln0  6419  ordsssuc  6453  onsssuc  6454  onnbtwn  6458  onunel  6469  suc11  6471  onun2  6472  ontr  6473  onordi  6475  onssneli  6479  epweon  7778  epweonALT  7779  ordeleqon  7785  onss  7788  sucexeloni  7812  onpwsuc  7816  onpsssuc  7819  onsucmin  7821  ordunpr  7826  ordunisuc  7832  onsucuni2  7834  onuniorsuc  7837  ordunisuc2  7844  ordzsl  7845  onzsl  7846  nlimon  7851  tfinds  7860  tfindsg2  7862  nnord  7874  poseq  8160  soseq  8161  onfununi  8334  smo11  8357  smoord  8358  smoword  8359  smogt  8360  tfrlem1  8368  tfrlem9a  8379  tfrlem15  8385  tz7.44-2  8400  tz7.48lem  8434  ord3  8475  oe0m1  8512  oaordi  8537  oaord  8538  oacan  8539  oawordri  8541  oalimcl  8551  oaass  8552  omord2  8558  omcan  8560  omwordi  8562  omword1  8564  omword2  8565  om00  8566  omlimcl  8569  omass  8571  omeulem2  8574  omopth2  8575  oen0  8578  oeord  8580  oecan  8581  oewordi  8583  oeworde  8585  oelimcl  8592  oeeulem  8593  oeeui  8594  nnarcl  8608  nnawordi  8613  nnawordex  8629  oaabs2  8641  omabs  8643  omsmo  8650  cofonr  8666  naddcllem  8668  naddsuc2  8694  omxpenlem  9080  infensuc  9157  dif1enlem  9158  nndomog  9211  onomeneq  9212  ordiso  9492  ordtypelem2  9495  hartogslem1  9518  cantnflt  9655  cantnfp1lem3  9663  cantnfp1  9664  oemapso  9665  oemapvali  9667  cantnflem1d  9671  cantnflem1  9672  cantnf  9676  oemapwe  9677  cantnffval2  9678  cnfcom  9683  r111  9761  r1ordg  9764  rankonidlem  9814  bndrank  9827  r1pw  9831  r1pwALT  9832  rankbnd2  9855  tcrank  9870  cardprclem  9988  carduni  9990  cardmin2  10008  infxpenlem  10020  alephdom  10088  alephdom2  10094  cardaleph  10096  iscard3  10100  alephfp  10115  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  10706  r1limwun  10749  r1wunlim  10750  tsksuc  10775  inar1  10788  gruina  10831  grur1a  10832  grur1  10833  nodmord  27897  noextendseq  27911  noextenddif  27912  nosupno  27947  nosupbday  27949  nosupres  27951  noinfno  27962  noinfbday  27964  noinfres  27966  noetasuplem4  27980  noetainflem4  27984  newbday  28175  oldfib  28650  fineqvnttrclse  35658  dfrdg2  36380  nmulprop  36778  ontgval  37058  ontgsucval  37059  onsuctopon  37061  onintopssconn  37067  onsuct0  37068  sucneqond  38127  onsucuni3  38129  aomclem4  43906  aomclem5  43907  onintunirab  44076  omlimcl2  44091  onelord  44100  ordeldifsucon  44108  ordeldif1o  44109  onsucss  44115  onsucf1olem  44119  onov0suclim  44123  oe0rif  44134  onsucwordi  44137  oege1  44155  cantnfresb  44173  omabs2  44181  ordsssucb  44184  tfsconcatlem  44185  tfsconcatfv2  44189  tfsconcatrn  44191  tfsconcatb0  44193  tfsconcat0b  44195  tfsconcatrev  44197  onsucunipr  44221  oaun3lem1  44223  oaun3lem2  44224  nadd1suc  44241  naddgeoa  44243  oaltom  44253  omltoe  44255  nlimsuc  44289  dfsucon  44371  minregex  44382  onfrALTlem3  45375  onfrALTlem2  45377  onfrALTlem3VD  45717  onfrALTlem2VD  45719  onsetreclem3  50641