MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexlimivw Unicode version

Theorem rexlimivw 2676
Description: Weaker version of rexlimiv 2674. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
rexlimivw  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3  |-  ( ph  ->  ps )
21a1i 10 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2674 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  eliun  3925  reusv3i  4557  reusv7OLD  4562  onuninsuci  4647  elrnmptg  4945  fun11iun  5509  fvelrnb  5586  fvelimab  5594  iinpreima  5671  fmpt  5697  fliftfun  5827  elrnmpt2  5973  ovelrn  6012  releldm2  6186  tfrlem4  6411  abianfp  6487  iiner  6747  elixpsn  6871  isfi  6901  card2on  7284  tz9.12lem1  7475  rankwflemb  7481  rankxpsuc  7568  scott0  7572  isnum2  7594  cardiun  7631  cardalephex  7733  dfac5lem4  7769  dfac12k  7789  cflim2  7905  cfss  7907  cfslb2n  7910  enfin2i  7963  fin23lem30  7984  itunitc  8063  axdc3lem2  8093  iundom2g  8178  pwcfsdom  8221  cfpwsdom  8222  tskr1om2  8406  gruiun  8437  genpelv  8640  prlem934  8673  suplem1pr  8692  supexpr  8694  supsrlem  8749  supsr  8750  fimaxre3  9719  iswrd  11431  caurcvgr  12162  caurcvg  12165  caucvg  12167  vdwapval  13036  restsspw  13352  mreunirn  13519  brssc  13707  arwhoma  13893  gexcl3  14914  dvdsr  15444  lspsnel  15776  lspprel  15863  iincld  16792  ssnei  16863  neindisj2  16876  lecldbas  16965  tgcnp  16999  cncnp2  17026  lmmo  17124  is2ndc  17188  fbfinnfr  17552  fbunfip  17580  filunirn  17593  fbflim2  17688  flimcls  17696  hauspwpwf1  17698  flftg  17707  isfcls  17720  fclsbas  17732  isfcf  17745  xmetunirn  17918  metss  18070  metrest  18086  qdensere  18295  elpi1  18559  lmmbr  18700  caun0  18723  nulmbl2  18910  itg2l  19100  aannenlem2  19725  taylfval  19754  ulmcl  19776  ulmpm  19778  ulmss  19790  hhcms  21798  hhsscms  21872  occllem  21898  occl  21899  chscllem2  22233  rabfmpunirn  23232  tpr2rico  23311  esumcst  23451  esumpcvgval  23461  esumcvg  23469  sigaclcuni  23494  mbfmfun  23574  rellyscon  23797  cvmliftlem15  23844  iseupa  23896  orderseqlem  24323  nofun  24374  norn  24376  dfrdg4  24560  brcolinear2  24753  brcolinear  24754  ellines  24847  r19.2zr  25060  eqfnung2  25221  sallnei  25632  intopcoaconlem3b  25641  intopcoaconlem3  25642  intopcoaconb  25643  vtarsuelt  25998  indcls2  26099  fnckleb  26149  elhalop2  26172  isibg2a1  26222  isibg2a2  26223  isibg2a3  26224  unirep  26452  filbcmb  26535  ellspd  27357  rngunsnply  27481  3v3e3cycl1  28390  bnj66  29208  bnj517  29233  islshpkrN  29932  ispointN  30553  pmapglbx  30580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator