Theorem rexlimivw 3144

Description: Weaker version of rexlimiv 3141. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)

Hypothesis

Ref	Expression
rexlimivw.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
rexlimivw	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 482	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3140	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3069

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  r19.36v  3176  r19.45v  3185  r19.44v  3186  r19.29vvaOLD  3204  sbcreu  3835  eliun  4963  reusv3i  5364  elrnmptg  5919  fvelrnb  6908  fvelimab  6919  iinpreima  7024  fmpt  7063  fliftfun  7262  elrnmpo  7497  ovelrn  7535  onuninsuci  7781  fiunlem  7879  releldm2  7980  poxp2  8080  poxp3  8087  orderseqlem  8094  tfrlem4  8330  naddunif  8644  iiner  8735  elixpsn  8882  isfi  8923  card2on  9499  brttrcl  9658  tz9.12lem1  9732  rankwflemb  9738  rankxpsuc  9827  scott0  9831  isnum2  9890  cardiun  9927  cardalephex  10035  dfac5lem4  10071  dfac12k  10092  cflim2  10208  cfss  10210  cfslb2n  10213  enfin2i  10266  fin23lem30  10287  itunitc  10366  axdc3lem2  10396  iundom2g  10485  pwcfsdom  10528  cfpwsdom  10529  tskr1om2  10713  genpelv  10945  prlem934  10978  suplem1pr  10997  supexpr  10999  supsrlem  11056  supsr  11057  fimaxre3  12110  iswrd  14416  caurcvgr  15570  caurcvg  15573  caucvg  15575  vdwapval  16856  restsspw  17327  mreunirn  17495  brssc  17711  arwhoma  17945  gexcl3  19383  dvdsr  20089  rhmdvdsr  20197  lspsnel  20521  lspprel  20612  ellspd  21245  iincld  22427  ssnei  22498  neindisj2  22511  neitr  22568  lecldbas  22607  tgcnp  22641  cncnp2  22669  lmmo  22768  is2ndc  22834  fbfinnfr  23229  fbunfip  23257  filunirn  23270  fbflim2  23365  flimcls  23373  hauspwpwf1  23375  flftg  23384  isfcls  23397  fclsbas  23409  isfcf  23422  ustfilxp  23601  ustbas  23616  restutop  23626  ucnima  23670  xmetunirn  23727  metss  23901  metrest  23917  restmetu  23963  qdensere  24170  elpi1  24445  lmmbr  24659  caun0  24682  nulmbl2  24937  itg2l  25131  aannenlem2  25726  taylfval  25755  ulmcl  25777  ulmpm  25779  ulmss  25793  nofun  27034  norn  27036  madeval2  27226  elmade  27240  tglnunirn  27553  ishpg  27764  edglnl  28157  uhgrwkspthlem1  28764  usgr2pth  28775  umgr2wlk  28957  elwwlks2ons3  28963  clwwlknun  29119  frgrncvvdeqlem3  29308  frgr2wwlkn0  29335  frgrreg  29401  hhcms  30208  hhsscms  30283  occllem  30308  occl  30309  chscllem2  30643  r19.29ffa  31465  rabfmpunirn  31636  kerunit  32185  tpr2rico  32582  gsumesum  32747  esumcst  32751  esumfsup  32758  esumpcvgval  32766  esumcvg  32774  sigaclcuni  32806  mbfmfun  32941  dya2icoseg2  32967  bnj66  33561  bnj517  33586  cusgr3cyclex  33817  rellysconn  33932  cvmliftlem15  33979  satffunlem2lem1  34085  dfrdg4  34612  brcolinear2  34719  brcolinear  34720  ellines  34813  poimirlem29  36180  volsupnfl  36196  unirep  36245  filbcmb  36272  islshpkrN  37655  ispointN  38278  pmapglbx  38305  rngunsnply  41558  elsetpreimafvbi  45703