Theorem rexlimivw 3150

Description: Weaker version of rexlimiv 3147. (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 481	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3146	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  r19.36v  3182  r19.45v  3191  r19.44v  3192  r19.29vvaOLD  3213  sbcreu  3870  eliun  5001  reusv3i  5402  elrnmptg  5958  fvelrnb  6952  fvelimab  6964  iinpreima  7070  fmpt  7111  fliftfun  7312  elrnmpo  7548  ovelrn  7587  onuninsuci  7833  fiunlem  7932  releldm2  8033  poxp2  8133  poxp3  8140  orderseqlem  8147  tfrlem4  8383  naddunif  8696  iiner  8787  elixpsn  8935  isfi  8976  card2on  9553  brttrcl  9712  tz9.12lem1  9786  rankwflemb  9792  rankxpsuc  9881  scott0  9885  isnum2  9944  cardiun  9981  cardalephex  10089  dfac5lem4  10125  dfac12k  10146  cflim2  10262  cfss  10264  cfslb2n  10267  enfin2i  10320  fin23lem30  10341  itunitc  10420  axdc3lem2  10450  iundom2g  10539  pwcfsdom  10582  cfpwsdom  10583  tskr1om2  10767  genpelv  10999  prlem934  11032  suplem1pr  11051  supexpr  11053  supsrlem  11110  supsr  11111  fimaxre3  12165  iswrd  14471  caurcvgr  15625  caurcvg  15628  caucvg  15630  vdwapval  16911  restsspw  17382  mreunirn  17550  brssc  17766  arwhoma  18000  gexcl3  19497  dvdsr  20254  rhmdvdsr  20400  lspsnel  20759  lspprel  20850  ellspd  21577  iincld  22764  ssnei  22835  neindisj2  22848  neitr  22905  lecldbas  22944  tgcnp  22978  cncnp2  23006  lmmo  23105  is2ndc  23171  fbfinnfr  23566  fbunfip  23594  filunirn  23607  fbflim2  23702  flimcls  23710  hauspwpwf1  23712  flftg  23721  isfcls  23734  fclsbas  23746  isfcf  23759  ustfilxp  23938  ustbas  23953  restutop  23963  ucnima  24007  xmetunirn  24064  metss  24238  metrest  24254  restmetu  24300  qdensere  24507  elpi1  24793  lmmbr  25007  caun0  25030  nulmbl2  25286  itg2l  25480  aannenlem2  26079  taylfval  26108  ulmcl  26130  ulmpm  26132  ulmss  26146  nofun  27389  norn  27391  madeval2  27586  elmade  27600  tglnunirn  28067  ishpg  28278  edglnl  28671  uhgrwkspthlem1  29278  usgr2pth  29289  umgr2wlk  29471  elwwlks2ons3  29477  clwwlknun  29633  frgrncvvdeqlem3  29822  frgr2wwlkn0  29849  frgrreg  29915  hhcms  30724  hhsscms  30799  occllem  30824  occl  30825  chscllem2  31159  r19.29ffa  31981  rabfmpunirn  32146  kerunit  32708  tpr2rico  33191  gsumesum  33356  esumcst  33360  esumfsup  33367  esumpcvgval  33375  esumcvg  33383  sigaclcuni  33415  mbfmfun  33550  dya2icoseg2  33576  bnj66  34170  bnj517  34195  cusgr3cyclex  34426  rellysconn  34541  cvmliftlem15  34588  satffunlem2lem1  34694  dfrdg4  35228  brcolinear2  35335  brcolinear  35336  ellines  35429  poimirlem29  36821  volsupnfl  36837  unirep  36886  filbcmb  36912  islshpkrN  38294  ispointN  38917  pmapglbx  38944  rngunsnply  42218  elsetpreimafvbi  46358