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

Theorem rexlimivw 2663
Description: Weaker version of rexlimiv 2661. (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 2661 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  eliun  3909  reusv3i  4541  reusv7OLD  4546  onuninsuci  4631  elrnmptg  4929  fun11iun  5493  fvelrnb  5570  fvelimab  5578  iinpreima  5655  fmpt  5681  fliftfun  5811  elrnmpt2  5957  ovelrn  5996  releldm2  6170  tfrlem4  6395  abianfp  6471  iiner  6731  elixpsn  6855  isfi  6885  card2on  7268  tz9.12lem1  7459  rankwflemb  7465  rankxpsuc  7552  scott0  7556  isnum2  7578  cardiun  7615  cardalephex  7717  dfac5lem4  7753  dfac12k  7773  cflim2  7889  cfss  7891  cfslb2n  7894  enfin2i  7947  fin23lem30  7968  itunitc  8047  axdc3lem2  8077  iundom2g  8162  pwcfsdom  8205  cfpwsdom  8206  tskr1om2  8390  gruiun  8421  genpelv  8624  prlem934  8657  suplem1pr  8676  supexpr  8678  supsrlem  8733  supsr  8734  fimaxre3  9703  iswrd  11415  caurcvgr  12146  caurcvg  12149  caucvg  12151  vdwapval  13020  restsspw  13336  mreunirn  13503  brssc  13691  arwhoma  13877  gexcl3  14898  dvdsr  15428  lspsnel  15760  lspprel  15847  iincld  16776  ssnei  16847  neindisj2  16860  lecldbas  16949  tgcnp  16983  cncnp2  17010  lmmo  17108  is2ndc  17172  fbfinnfr  17536  fbunfip  17564  filunirn  17577  fbflim2  17672  flimcls  17680  hauspwpwf1  17682  flftg  17691  isfcls  17704  fclsbas  17716  isfcf  17729  xmetunirn  17902  metss  18054  metrest  18070  qdensere  18279  elpi1  18543  lmmbr  18684  caun0  18707  nulmbl2  18894  itg2l  19084  aannenlem2  19709  taylfval  19738  ulmcl  19760  ulmpm  19762  ulmss  19774  hhcms  21782  hhsscms  21856  occllem  21882  occl  21883  chscllem2  22217  rabfmpunirn  23217  tpr2rico  23296  esumcst  23436  esumpcvgval  23446  esumcvg  23454  sigaclcuni  23479  mbfmfun  23559  rellyscon  23782  cvmliftlem15  23829  iseupa  23881  orderseqlem  24252  nofun  24303  norn  24305  dfrdg4  24488  brcolinear2  24681  brcolinear  24682  ellines  24775  r19.2zr  24957  eqfnung2  25118  sallnei  25529  intopcoaconlem3b  25538  intopcoaconlem3  25539  intopcoaconb  25540  vtarsuelt  25895  indcls2  25996  fnckleb  26046  elhalop2  26069  isibg2a1  26119  isibg2a2  26120  isibg2a3  26121  unirep  26349  filbcmb  26432  ellspd  27254  rngunsnply  27378  bnj66  28892  bnj517  28917  islshpkrN  29310  ispointN  29931  pmapglbx  29958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator