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

Theorem rexlimivw 2952
Description: Weaker version of rexlimiv 2949. (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 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2949 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  r19.29_2a  3005  sbcreu  3418  eliun  4330  reusv3i  4654  reusv7OLD  4659  elrnmptg  5252  fvelrnb  5915  fvelimab  5923  iinpreima  6011  fmpt  6042  fliftfun  6198  elrnmpt2  6399  ovelrn  6435  onuninsuci  6659  fun11iun  6744  releldm2  6834  tfrlem4  7048  iiner  7383  elixpsn  7508  isfi  7539  card2on  7980  tz9.12lem1  8205  rankwflemb  8211  rankxpsuc  8300  scott0  8304  isnum2  8326  cardiun  8363  cardalephex  8471  dfac5lem4  8507  dfac12k  8527  cflim2  8643  cfss  8645  cfslb2n  8648  enfin2i  8701  fin23lem30  8722  itunitc  8801  axdc3lem2  8831  iundom2g  8915  pwcfsdom  8958  cfpwsdom  8959  tskr1om2  9146  gruiun  9177  genpelv  9378  prlem934  9411  suplem1pr  9430  supexpr  9432  supsrlem  9488  supsr  9489  fimaxre3  10492  iswrd  12516  caurcvgr  13459  caurcvg  13462  caucvg  13464  vdwapval  14350  restsspw  14687  mreunirn  14856  brssc  15044  arwhoma  15230  gexcl3  16413  dvdsr  17096  lspsnel  17449  lspprel  17540  ellspd  18631  ellspdOLD  18632  iincld  19334  ssnei  19405  neindisj2  19418  neitr  19475  lecldbas  19514  tgcnp  19548  cncnp2  19576  lmmo  19675  is2ndc  19741  fbfinnfr  20105  fbunfip  20133  filunirn  20146  fbflim2  20241  flimcls  20249  hauspwpwf1  20251  flftg  20260  isfcls  20273  fclsbas  20285  isfcf  20298  ustfilxp  20478  ustbas  20493  restutop  20503  ucnima  20547  xmetunirn  20603  metss  20774  metrest  20790  restmetu  20853  qdensere  21040  elpi1  21308  lmmbr  21460  caun0  21483  nulmbl2  21710  itg2l  21899  aannenlem2  22487  taylfval  22516  ulmcl  22538  ulmpm  22540  ulmss  22554  tglnunirn  23691  3v3e3cycl1  24348  iseupa  24669  frgrancvvdeqlem4  24738  frg2wotn0  24761  usgreghash2spot  24774  hhcms  25824  hhsscms  25899  occllem  25925  occl  25926  chscllem2  26260  rabfmpunirn  27191  rhmdvdsr  27499  kerunit  27504  tpr2rico  27558  gsumesum  27735  esumcst  27739  esumfsup  27744  esumpcvgval  27752  esumcvg  27760  sigaclcuni  27786  mbfmfun  27893  dya2icoseg2  27917  rellyscon  28364  cvmliftlem15  28411  orderseqlem  28937  nofun  29014  norn  29016  dfrdg4  29205  brcolinear2  29313  brcolinear  29314  ellines  29407  volsupnfl  29664  unirep  29834  filbcmb  29862  rngunsnply  30755  usgra2pth  31849  bnj66  33015  bnj517  33040  islshpkrN  33935  ispointN  34556  pmapglbx  34583
  Copyright terms: Public domain W3C validator