Theorem eloni 6176

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

Syntax hints:   → wi 4   ∈ wcel 2113  Ord word 6165  Oncon0 6166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-v 3399  df-in 3848  df-ss 3858  df-uni 4794  df-tr 5134  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6169  df-on 6170

This theorem is referenced by:  onelon  6191  onin  6197  ontri1  6200  onfr  6205  onelpss  6206  onsseleq  6207  onelss  6208  ontr1  6212  ontr2  6213  ordunidif  6214  on0eln0  6221  ordsssuc  6252  onsssuc  6253  onnbtwn  6257  suc11  6269  onun2  6270  onordi  6271  onssneli  6276  epweon  7510  ordeleqon  7516  onss  7518  ordsuc  7542  onpwsuc  7544  onpsssuc  7547  onsucmin  7549  ordunpr  7554  ordunisuc  7560  onsucuni2  7562  onuninsuci  7568  ordunisuc2  7572  ordzsl  7573  onzsl  7574  nlimon  7579  tfinds  7587  tfindsg2  7589  nnord  7601  onfununi  8000  smo11  8023  smoord  8024  smoword  8025  smogt  8026  tfrlem1  8034  tfrlem9a  8044  tfrlem15  8050  tz7.44-2  8065  tz7.48lem  8099  oe0m1  8170  oaordi  8196  oaord  8197  oacan  8198  oawordri  8200  oalimcl  8210  oaass  8211  omord2  8217  omcan  8219  omwordi  8221  omword1  8223  omword2  8224  om00  8225  omlimcl  8228  omass  8230  omeulem2  8233  omopth2  8234  oen0  8236  oeord  8238  oecan  8239  oewordi  8241  oeworde  8243  oelimcl  8250  oeeulem  8251  oeeui  8252  nnarcl  8266  nnawordi  8271  nnawordex  8287  oaabs2  8296  omabs  8298  omsmo  8305  omxpenlem  8660  infensuc  8738  nndomog  8751  onomeneq  8781  ordiso  9046  ordtypelem2  9049  hartogslem1  9072  cantnflt  9201  cantnfp1lem3  9209  cantnfp1  9210  oemapso  9211  oemapvali  9213  cantnflem1d  9217  cantnflem1  9218  cantnf  9222  oemapwe  9223  cantnffval2  9224  cnfcom  9229  r111  9270  r1ordg  9273  rankonidlem  9323  bndrank  9336  r1pw  9340  r1pwALT  9341  rankbnd2  9364  tcrank  9379  cardprclem  9474  carduni  9476  cardmin2  9494  infxpenlem  9506  alephdom  9574  alephdom2  9580  cardaleph  9582  iscard3  9586  alephfp  9601  dfac12lem1  9636  dfac12lem2  9637  dfac12lem3  9638  cflim2  9756  cofsmo  9762  cfsmolem  9763  coftr  9766  cfcof  9767  fin67  9888  hsmexlem5  9923  zorn2lem6  9994  ttukeylem3  10004  ttukeylem5  10006  ttukeylem6  10007  ttukeylem7  10008  winainflem  10186  r1limwun  10229  r1wunlim  10230  tsksuc  10255  inar1  10268  gruina  10311  grur1a  10312  grur1  10313  onunel  33255  dfrdg2  33335  poseq  33405  soseq  33406  naddcllem  33464  nodmord  33489  noextendseq  33503  noextenddif  33504  nosupno  33539  nosupbday  33541  nosupres  33543  noinfno  33554  noinfbday  33556  noinfres  33558  noetasuplem4  33572  noetainflem4  33576  newbday  33712  ontgval  34250  ontgsucval  34251  onsuctopon  34253  onintopssconn  34259  onsuct0  34260  sucneqond  35148  onsucuni3  35150  aomclem4  40438  aomclem5  40439  dfsucon  40668  onfrALTlem3  41686  onfrALTlem2  41688  onfrALTlem3VD  42029  onfrALTlem2VD  42031  onsetreclem3  45849