MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eloni Structured version   Visualization version   GIF version

Theorem eloni 6174
Description: An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
eloni (𝐴 ∈ On → Ord 𝐴)

Proof of Theorem eloni
StepHypRef Expression
1 elong 6172 . 2 (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
21ibi 270 1 (𝐴 ∈ On → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  Ord word 6163  Oncon0 6164
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-v 3473  df-in 3917  df-ss 3927  df-uni 4812  df-tr 5146  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-ord 6167  df-on 6168
This theorem is referenced by:  onelon  6189  onin  6195  ontri1  6198  onfr  6203  onelpss  6204  onsseleq  6205  onelss  6206  ontr1  6210  ontr2  6211  ordunidif  6212  on0eln0  6219  ordsssuc  6250  onsssuc  6251  onnbtwn  6255  suc11  6267  onordi  6268  onssneli  6273  epweon  7472  ordeleqon  7478  onss  7480  ordsuc  7504  onpwsuc  7506  onpsssuc  7509  onsucmin  7511  ordunpr  7516  ordunisuc  7522  onsucuni2  7524  onuninsuci  7530  ordunisuc2  7534  ordzsl  7535  onzsl  7536  nlimon  7541  tfinds  7549  tfindsg2  7551  nnord  7563  onfununi  7953  smo11  7976  smoord  7977  smoword  7978  smogt  7979  tfrlem1  7987  tfrlem9a  7997  tfrlem15  8003  tz7.44-2  8018  tz7.48lem  8052  oe0m1  8121  oaordi  8147  oaord  8148  oacan  8149  oawordri  8151  oalimcl  8161  oaass  8162  omord2  8168  omcan  8170  omwordi  8172  omword1  8174  omword2  8175  om00  8176  omlimcl  8179  omass  8181  omeulem2  8184  omopth2  8185  oen0  8187  oeord  8189  oecan  8190  oewordi  8192  oeworde  8194  oelimcl  8201  oeeulem  8202  oeeui  8203  nnarcl  8217  nnawordi  8222  nnawordex  8238  oaabs2  8247  omabs  8249  omsmo  8256  omxpenlem  8593  infensuc  8671  nndomog  8684  onomeneq  8685  ordiso  8956  ordtypelem2  8959  hartogslem1  8982  cantnflt  9111  cantnfp1lem3  9119  cantnfp1  9120  oemapso  9121  oemapvali  9123  cantnflem1d  9127  cantnflem1  9128  cantnf  9132  oemapwe  9133  cantnffval2  9134  cnfcom  9139  r111  9180  r1ordg  9183  rankonidlem  9233  bndrank  9246  r1pw  9250  r1pwALT  9251  rankbnd2  9274  tcrank  9289  cardprclem  9384  carduni  9386  cardmin2  9404  infxpenlem  9416  alephdom  9484  alephdom2  9490  cardaleph  9492  iscard3  9496  alephfp  9511  dfac12lem1  9546  dfac12lem2  9547  dfac12lem3  9548  cflim2  9662  cofsmo  9668  cfsmolem  9669  coftr  9672  cfcof  9673  fin67  9794  hsmexlem5  9829  zorn2lem6  9900  ttukeylem3  9910  ttukeylem5  9912  ttukeylem6  9913  ttukeylem7  9914  winainflem  10092  r1limwun  10135  r1wunlim  10136  tsksuc  10161  inar1  10174  gruina  10217  grur1a  10218  grur1  10219  dfrdg2  33048  poseq  33103  soseq  33104  nodmord  33168  noextendseq  33182  noextenddif  33183  nosupno  33211  nosupres  33215  noetalem3  33227  ontgval  33787  ontgsucval  33788  onsuctopon  33790  onintopssconn  33796  onsuct0  33797  sucneqond  34666  onsucuni3  34668  aomclem4  39808  aomclem5  39809  dfsucon  40038  onfrALTlem3  41061  onfrALTlem2  41063  onfrALTlem3VD  41404  onfrALTlem2VD  41406  onsetreclem3  45043
  Copyright terms: Public domain W3C validator