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

Theorem eloni 5895
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 5893 . 2 (𝐴 ∈ On → (𝐴 ∈ On ↔ Ord 𝐴))
21ibi 256 1 (𝐴 ∈ On → Ord 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2140  Ord word 5884  Oncon0 5885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-rex 3057  df-v 3343  df-in 3723  df-ss 3730  df-uni 4590  df-tr 4906  df-po 5188  df-so 5189  df-fr 5226  df-we 5228  df-ord 5888  df-on 5889
This theorem is referenced by:  onelon  5910  onin  5916  ontri1  5919  onfr  5925  onelpss  5926  onsseleq  5927  onelss  5928  ontr1  5933  ontr2  5934  ordunidif  5935  on0eln0  5942  ordsssuc  5974  onsssuc  5975  onnbtwn  5980  suc11  5993  onordi  5994  onssneli  5999  ordon  7149  ordeleqon  7155  onss  7157  ordsuc  7181  onpwsuc  7183  onpsssuc  7186  onsucmin  7188  ordunpr  7193  ordunisuc  7199  onsucuni2  7201  onuninsuci  7207  ordunisuc2  7211  ordzsl  7212  onzsl  7213  nlimon  7218  tfinds  7226  tfindsg2  7228  nnord  7240  onfununi  7609  smo11  7632  smoord  7633  smoword  7634  smogt  7635  tfrlem1  7643  tfrlem9a  7653  tfrlem15  7659  tz7.44-2  7674  tz7.48lem  7707  oe0m1  7773  oaordi  7798  oaord  7799  oacan  7800  oawordri  7802  oalimcl  7812  oaass  7813  omord2  7819  omcan  7821  omwordi  7823  omword1  7825  omword2  7826  om00  7827  omlimcl  7830  omass  7832  omeulem2  7835  omopth2  7836  oen0  7838  oeord  7840  oecan  7841  oewordi  7843  oeworde  7845  oelimcl  7852  oeeulem  7853  oeeui  7854  nnarcl  7868  nnawordi  7873  nnawordex  7889  oaabs2  7897  omabs  7899  omsmo  7906  omxpenlem  8229  infensuc  8306  onomeneq  8318  ordiso  8589  ordtypelem2  8592  hartogslem1  8615  cantnflt  8745  cantnfp1lem3  8753  cantnfp1  8754  oemapso  8755  oemapvali  8757  cantnflem1d  8761  cantnflem1  8762  cantnf  8766  oemapwe  8767  cantnffval2  8768  cnfcom  8773  r111  8814  r1ordg  8817  rankonidlem  8867  bndrank  8880  r1pw  8884  r1pwALT  8885  rankbnd2  8908  tcrank  8923  cardprclem  9016  carduni  9018  cardmin2  9035  infxpenlem  9047  alephdom  9115  alephdom2  9121  cardaleph  9123  iscard3  9127  alephfp  9142  dfac12lem1  9178  dfac12lem2  9179  dfac12lem3  9180  cflim2  9298  cofsmo  9304  cfsmolem  9305  coftr  9308  cfcof  9309  fin67  9430  hsmexlem5  9465  zorn2lem6  9536  ttukeylem3  9546  ttukeylem5  9548  ttukeylem6  9549  ttukeylem7  9550  winainflem  9728  r1limwun  9771  r1wunlim  9772  tsksuc  9797  inar1  9810  gruina  9853  grur1a  9854  grur1  9855  dfrdg2  32028  poseq  32081  soseq  32082  nodmord  32134  noextendseq  32148  noextenddif  32149  nosupno  32177  nosupres  32181  noetalem3  32193  ontgval  32758  ontgsucval  32759  onsuctopon  32761  onintopssconn  32767  onsuct0  32768  sucneqond  33543  onsucuni3  33545  aomclem4  38148  aomclem5  38149  onfrALTlem3  39280  onfrALTlem2  39282  onfrALTlem3VD  39641  onfrALTlem2VD  39643  onsetreclem3  42982
  Copyright terms: Public domain W3C validator