Theorem eloni 6365

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-uni 4868  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6358  df-on 6359

This theorem is used by:  onelon  6380  onin  6387  ontri1  6390  onfr  6395  onelpss  6396  onsseleq  6397  onelss  6398  oneltri  6399  ontr1  6403  ontr2  6404  ordunidif  6406  on0eln0  6413  ordsssuc  6447  onsssuc  6448  onnbtwn  6452  onunel  6463  suc11  6465  onun2  6466  ontr  6467  onordi  6469  onssneli  6473  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  8159  soseq  8160  onfununi  8333  smo11  8356  smoord  8357  smoword  8358  smogt  8359  tfrlem1  8367  tfrlem9a  8378  tfrlem15  8384  tz7.44-2  8399  onelfvnef1  8433  tz7.48lemOLD  8435  ord3  8476  oe0m1  8513  oaordi  8538  oaord  8539  oacan  8540  oawordri  8542  oalimcl  8552  oaass  8553  omord2  8559  omcan  8561  omwordi  8563  omword1  8565  omword2  8566  om00  8567  omlimcl  8570  omass  8572  omeulem2  8575  omopth2  8576  oen0  8579  oeord  8581  oecan  8582  oewordi  8584  oeworde  8586  oelimcl  8593  oeeulem  8594  oeeui  8595  nnarcl  8609  nnawordi  8614  nnawordex  8630  oaabs2  8642  omabs  8644  omsmo  8651  cofonr  8667  naddcllem  8669  naddsuc2  8695  omxpenlem  9081  infensuc  9158  dif1enlem  9159  nndomog  9212  onomeneq  9213  ordiso  9494  ordtypelem2  9497  hartogslem1  9520  cantnflt  9657  cantnfp1lem3  9665  cantnfp1  9666  oemapso  9667  oemapvali  9669  cantnflem1d  9673  cantnflem1  9674  cantnf  9678  oemapwe  9679  cantnffval2  9680  cnfcom  9685  r111  9765  r1ordg  9768  rankonidlem  9819  bndrank  9835  r1pw  9840  r1pwALT  9841  rankbnd2  9867  tcrank  9882  cardprclem  10041  carduni  10043  cardmin2  10061  infxpenlem  10073  alephdom  10141  alephdom2  10147  cardaleph  10149  iscard3  10153  alephfp  10168  dfac12lem1  10203  dfac12lem2  10204  dfac12lem3  10205  cflim2  10322  cofsmo  10328  cfsmolem  10329  coftr  10332  cfcof  10333  fin67  10454  hsmexlem5  10489  zorn2lem6  10560  ttukeylem3  10570  ttukeylem5  10572  ttukeylem6  10573  ttukeylem7  10574  winainflem  10759  r1limwun  10802  r1wunlim  10803  tsksuc  10828  inar1  10841  gruina  10884  grur1a  10885  grur1  10886  nodmord  27992  noextendseq  28006  noextenddif  28007  nosupno  28042  nosupbday  28044  nosupres  28046  noinfno  28057  noinfbday  28059  noinfres  28061  noetasuplem4  28075  noetainflem4  28079  newbday  28270  oldfib  28745  fineqvnttrclse  35765  dfrdg2  36527  nmulprop  36909  ontgval  37189  ontgsucval  37190  onsuctopon  37192  onintopssconn  37198  onsuct0  37199  sucneqond  38256  onsucuni3  38258  aomclem4  44017  aomclem5  44018  onintunirab  44187  omlimcl2  44202  onelord  44211  ordeldifsucon  44219  ordeldif1o  44220  onsucss  44226  onsucf1olem  44230  onov0suclim  44234  oe0rif  44245  onsucwordi  44248  oege1  44266  cantnfresb  44284  omabs2  44292  ordsssucb  44295  tfsconcatlem  44296  tfsconcatfv2  44300  tfsconcatrn  44302  tfsconcatb0  44304  tfsconcat0b  44306  tfsconcatrev  44308  onsucunipr  44332  oaun3lem1  44334  oaun3lem2  44335  nadd1suc  44352  naddgeoa  44354  oaltom  44364  omltoe  44366  nlimsuc  44400  dfsucon  44482  minregex  44493  onfrALTlem3  45486  onfrALTlem2  45488  onfrALTlem3VD  45828  onfrALTlem2VD  45830  onsetreclem3  50744