Theorem eloni 6169

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

Syntax hints:   → wi 4   ∈ wcel 2111  Ord word 6158  Oncon0 6159

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-tr 5137  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6162  df-on 6163

This theorem is referenced by:  onelon  6184  onin  6190  ontri1  6193  onfr  6198  onelpss  6199  onsseleq  6200  onelss  6201  ontr1  6205  ontr2  6206  ordunidif  6207  on0eln0  6214  ordsssuc  6245  onsssuc  6246  onnbtwn  6250  suc11  6262  onordi  6263  onssneli  6268  epweon  7477  ordeleqon  7483  onss  7485  ordsuc  7509  onpwsuc  7511  onpsssuc  7514  onsucmin  7516  ordunpr  7521  ordunisuc  7527  onsucuni2  7529  onuninsuci  7535  ordunisuc2  7539  ordzsl  7540  onzsl  7541  nlimon  7546  tfinds  7554  tfindsg2  7556  nnord  7568  onfununi  7961  smo11  7984  smoord  7985  smoword  7986  smogt  7987  tfrlem1  7995  tfrlem9a  8005  tfrlem15  8011  tz7.44-2  8026  tz7.48lem  8060  oe0m1  8129  oaordi  8155  oaord  8156  oacan  8157  oawordri  8159  oalimcl  8169  oaass  8170  omord2  8176  omcan  8178  omwordi  8180  omword1  8182  omword2  8183  om00  8184  omlimcl  8187  omass  8189  omeulem2  8192  omopth2  8193  oen0  8195  oeord  8197  oecan  8198  oewordi  8200  oeworde  8202  oelimcl  8209  oeeulem  8210  oeeui  8211  nnarcl  8225  nnawordi  8230  nnawordex  8246  oaabs2  8255  omabs  8257  omsmo  8264  omxpenlem  8601  infensuc  8679  nndomog  8692  onomeneq  8693  ordiso  8964  ordtypelem2  8967  hartogslem1  8990  cantnflt  9119  cantnfp1lem3  9127  cantnfp1  9128  oemapso  9129  oemapvali  9131  cantnflem1d  9135  cantnflem1  9136  cantnf  9140  oemapwe  9141  cantnffval2  9142  cnfcom  9147  r111  9188  r1ordg  9191  rankonidlem  9241  bndrank  9254  r1pw  9258  r1pwALT  9259  rankbnd2  9282  tcrank  9297  cardprclem  9392  carduni  9394  cardmin2  9412  infxpenlem  9424  alephdom  9492  alephdom2  9498  cardaleph  9500  iscard3  9504  alephfp  9519  dfac12lem1  9554  dfac12lem2  9555  dfac12lem3  9556  cflim2  9674  cofsmo  9680  cfsmolem  9681  coftr  9684  cfcof  9685  fin67  9806  hsmexlem5  9841  zorn2lem6  9912  ttukeylem3  9922  ttukeylem5  9924  ttukeylem6  9925  ttukeylem7  9926  winainflem  10104  r1limwun  10147  r1wunlim  10148  tsksuc  10173  inar1  10186  gruina  10229  grur1a  10230  grur1  10231  dfrdg2  33153  poseq  33208  soseq  33209  nodmord  33273  noextendseq  33287  noextenddif  33288  nosupno  33316  nosupres  33320  noetalem3  33332  ontgval  33892  ontgsucval  33893  onsuctopon  33895  onintopssconn  33901  onsuct0  33902  sucneqond  34782  onsucuni3  34784  aomclem4  40001  aomclem5  40002  dfsucon  40231  onfrALTlem3  41250  onfrALTlem2  41252  onfrALTlem3VD  41593  onfrALTlem2VD  41595  onsetreclem3  45236