Theorem eloni 6280

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

Syntax hints:   → wi 4   ∈ wcel 2107  Ord word 6269  Oncon0 6270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-tr 5193  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-ord 6273  df-on 6274

This theorem is referenced by:  onelon  6295  onin  6301  ontri1  6304  onfr  6309  onelpss  6310  onsseleq  6311  onelss  6312  ontr1  6316  ontr2  6317  ordunidif  6318  on0eln0  6325  ordsssuc  6356  onsssuc  6357  onnbtwn  6361  suc11  6373  onun2  6374  onordi  6375  onssneli  6380  epweon  7634  epweonOLD  7635  ordeleqon  7641  onss  7643  ordsuc  7670  onpwsuc  7672  onpsssuc  7675  onsucmin  7677  ordunpr  7682  ordunisuc  7688  onsucuni2  7690  onuninsuci  7696  ordunisuc2  7700  ordzsl  7701  onzsl  7702  nlimon  7707  tfinds  7715  tfindsg2  7717  nnord  7729  onfununi  8181  smo11  8204  smoord  8205  smoword  8206  smogt  8207  tfrlem1  8216  tfrlem9a  8226  tfrlem15  8232  tz7.44-2  8247  tz7.48lem  8281  oe0m1  8360  oaordi  8386  oaord  8387  oacan  8388  oawordri  8390  oalimcl  8400  oaass  8401  omord2  8407  omcan  8409  omwordi  8411  omword1  8413  omword2  8414  om00  8415  omlimcl  8418  omass  8420  omeulem2  8423  omopth2  8424  oen0  8426  oeord  8428  oecan  8429  oewordi  8431  oeworde  8433  oelimcl  8440  oeeulem  8441  oeeui  8442  nnarcl  8456  nnawordi  8461  nnawordex  8477  oaabs2  8488  omabs  8490  omsmo  8497  omxpenlem  8869  infensuc  8951  nndomog  9008  nndomogOLD  9018  onomeneq  9020  onomeneqOLD  9021  ordiso  9284  ordtypelem2  9287  hartogslem1  9310  cantnflt  9439  cantnfp1lem3  9447  cantnfp1  9448  oemapso  9449  oemapvali  9451  cantnflem1d  9455  cantnflem1  9456  cantnf  9460  oemapwe  9461  cantnffval2  9462  cnfcom  9467  r111  9542  r1ordg  9545  rankonidlem  9595  bndrank  9608  r1pw  9612  r1pwALT  9613  rankbnd2  9636  tcrank  9651  cardprclem  9746  carduni  9748  cardmin2  9766  infxpenlem  9778  alephdom  9846  alephdom2  9852  cardaleph  9854  iscard3  9858  alephfp  9873  dfac12lem1  9908  dfac12lem2  9909  dfac12lem3  9910  cflim2  10028  cofsmo  10034  cfsmolem  10035  coftr  10038  cfcof  10039  fin67  10160  hsmexlem5  10195  zorn2lem6  10266  ttukeylem3  10276  ttukeylem5  10278  ttukeylem6  10279  ttukeylem7  10280  winainflem  10458  r1limwun  10501  r1wunlim  10502  tsksuc  10527  inar1  10540  gruina  10583  grur1a  10584  grur1  10585  onunel  33698  dfrdg2  33780  poseq  33811  soseq  33812  naddcllem  33840  nodmord  33865  noextendseq  33879  noextenddif  33880  nosupno  33915  nosupbday  33917  nosupres  33919  noinfno  33930  noinfbday  33932  noinfres  33934  noetasuplem4  33948  noetainflem4  33952  newbday  34091  ontgval  34629  ontgsucval  34630  onsuctopon  34632  onintopssconn  34638  onsuct0  34639  sucneqond  35545  onsucuni3  35547  aomclem4  40889  aomclem5  40890  nlimsuc  41055  dfsucon  41137  minregex  41148  onfrALTlem3  42171  onfrALTlem2  42173  onfrALTlem3VD  42514  onfrALTlem2VD  42516  onsetreclem3  46423