Theorem eloni 6372

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-uni 4867  df-tr 5212  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-ord 6365  df-on 6366

This theorem is used by:  onelon  6387  onin  6394  ontri1  6397  onfr  6402  onelpss  6403  onsseleq  6404  onelss  6405  oneltri  6406  ontr1  6410  ontr2  6411  ordunidif  6413  on0eln0  6420  ordsssuc  6454  onsssuc  6455  onnbtwn  6459  onunel  6470  suc11  6472  onun2  6473  ontr  6474  onordi  6476  onssneli  6480  epweon  7790  epweonALT  7791  ordeleqon  7797  onss  7800  sucexeloni  7824  onpwsuc  7828  onpsssuc  7831  onsucmin  7833  ordunpr  7838  onsucuni2  7846  onuniorsuc  7849  ordunisuc2  7856  ordzsl  7857  onzsl  7858  nlimon  7863  tfinds  7872  tfindsg2  7874  nnord  7886  poseq  8178  soseq  8179  onfununi  8353  smo11  8376  smoord  8377  smoword  8378  smogt  8379  tfrlem1  8387  tfrlem9a  8398  tfrlem15  8404  tz7.44-2  8419  onelfvnef1  8453  tz7.48lemOLD  8455  ord3  8496  oe0m1  8533  oaordi  8558  oaord  8559  oacan  8560  oawordri  8562  oalimcl  8572  oaass  8573  omord2  8579  omcan  8581  omwordi  8583  omword1  8585  omword2  8586  om00  8587  omlimcl  8590  omass  8592  omeulem2  8595  omopth2  8596  oen0  8599  oeord  8601  oecan  8602  oewordi  8604  oeworde  8606  oelimcl  8613  oeeulem  8614  oeeui  8615  nnarcl  8629  nnawordi  8634  nnawordex  8650  oaabs2  8662  omabs  8664  omsmo  8671  cofonr  8687  naddcllem  8689  naddsuc2  8715  omxpenlem  9101  infensuc  9178  dif1enlem  9179  nndomog  9232  onomeneq  9233  ordiso  9514  ordtypelem2  9517  hartogslem1  9540  cantnflt  9677  cantnfp1lem3  9685  cantnfp1  9686  oemapso  9687  oemapvali  9689  cantnflem1d  9693  cantnflem1  9694  cantnf  9698  oemapwe  9699  cantnffval2  9700  cnfcom  9705  r111  9786  r1ordg  9789  rankonidlem  9842  bndrank  9858  r1pw  9863  r1pwALT  9864  rankbnd2  9890  tcrank  9905  cardprclem  10064  carduni  10066  cardmin2  10084  infxpenlem  10096  alephdom  10164  alephdom2  10170  cardaleph  10172  iscard3  10176  alephfp  10191  dfac12lem1  10226  dfac12lem2  10227  dfac12lem3  10228  cflim2  10345  cofsmo  10351  cfsmolem  10352  coftr  10355  cfcof  10356  fin67  10477  hsmexlem5  10512  zorn2lem6  10583  ttukeylem3  10593  ttukeylem5  10595  ttukeylem6  10596  ttukeylem7  10597  winainflem  10782  r1limwun  10825  r1wunlim  10826  tsksuc  10851  inar1  10864  gruina  10907  grur1a  10908  grur1  10909  nodmord  28016  noextendseq  28030  noextenddif  28031  nosupno  28066  nosupbday  28068  nosupres  28070  noinfno  28081  noinfbday  28083  noinfres  28085  noetasuplem4  28099  noetainflem4  28103  newbday  28294  oldfib  28769  fineqvnttrclse  35849  maxssj0  35946  dfrdg2  36650  nmulprop  37032  ontgval  37312  ontgsucval  37313  onsuctopon  37315  onintopssconn  37321  onsuct0  37322  sucneqond  38382  onsucuni3  38384  aomclem4  44153  aomclem5  44154  onintunirab  44323  omlimcl2  44338  onelord  44347  ordeldifsucon  44355  ordeldif1o  44356  onsucss  44362  onsucf1olem  44366  onov0suclim  44370  oe0rif  44381  onsucwordi  44384  oege1  44402  cantnfresb  44420  omabs2  44428  ordsssucb  44431  tfsconcatlem  44432  tfsconcatfv2  44436  tfsconcatrn  44438  tfsconcatb0  44440  tfsconcat0b  44442  tfsconcatrev  44444  onsucunipr  44468  oaun3lem1  44470  oaun3lem2  44471  nadd1suc  44488  naddgeoa  44490  oaltom  44500  omltoe  44502  nlimsuc  44536  dfsucon  44618  minregex  44629  onfrALTlem3  45621  onfrALTlem2  45623  onfrALTlem3VD  45963  onfrALTlem2VD  45965  onsetreclem3  50969