Theorem rexlimivw 3136

Description: Weaker version of rexlimiv 3133. (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 3132	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  r19.36v  3167  r19.45v  3173  r19.44v  3174  sbcreu  3808  eliun  4925  reusv3i  5333  elrnmptg  5903  fvelrnb  6887  fvelimab  6899  iinpreima  7010  fmpt  7051  fliftfun  7256  elrnmpo  7492  ovelrn  7532  onuninsuci  7780  fiunlem  7884  releldm2  7985  poxp2  8083  poxp3  8090  orderseqlem  8097  tfrlem4  8308  naddunif  8619  iiner  8726  elixpsn  8875  isfi  8912  card2on  9459  brttrcl  9625  tz9.12lem1  9702  rankwflemb  9708  rankxpsuc  9797  scott0  9801  isnum2  9860  cardiun  9897  cardalephex  10003  dfac5lem4  10039  dfac5lem4OLD  10041  dfac12k  10061  cflim2  10176  cfss  10178  cfslb2n  10181  enfin2i  10234  fin23lem30  10255  itunitc  10334  axdc3lem2  10364  iundom2g  10453  pwcfsdom  10497  cfpwsdom  10498  tskr1om2  10682  genpelv  10914  prlem934  10947  suplem1pr  10966  supexpr  10968  supsrlem  11025  supsr  11026  fimaxre3  12093  iswrd  14468  caurcvgr  15627  caurcvg  15630  caucvg  15632  vdwapval  16935  restsspw  17385  mreunirn  17554  brssc  17772  arwhoma  18003  gexcl3  19553  dvdsr  20333  rhmdvdsr  20480  ellspsn  20993  lspprel  21084  ellspd  21777  iincld  23022  ssnei  23093  neindisj2  23106  neitr  23163  lecldbas  23202  tgcnp  23236  cncnp2  23264  lmmo  23363  is2ndc  23429  fbfinnfr  23824  fbunfip  23852  filunirn  23865  fbflim2  23960  flimcls  23968  hauspwpwf1  23970  flftg  23979  isfcls  23992  fclsbas  24004  isfcf  24017  ustfilxp  24196  ustbas  24210  restutop  24220  ucnima  24263  xmetunirn  24320  metss  24491  metrest  24507  restmetu  24553  qdensere  24752  elpi1  25030  lmmbr  25243  caun0  25266  nulmbl2  25521  itg2l  25714  aannenlem2  26313  taylfval  26342  ulmcl  26364  ulmpm  26366  ulmss  26380  elno  27627  nofun  27631  norn  27633  madeval2  27843  elmade  27867  tglnunirn  28634  ishpg  28845  edglnl  29230  uhgrwkspthlem1  29839  usgr2pth  29850  umgr2wlk  30035  elwwlks2ons3  30041  clwwlknun  30200  frgrncvvdeqlem3  30389  frgr2wwlkn0  30416  frgrreg  30482  hhcms  31292  hhsscms  31367  occllem  31392  occl  31393  chscllem2  31727  r19.29ffa  32558  rabfmpunirn  32745  kerunit  33408  tpr2rico  34096  gsumesum  34243  esumcst  34247  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  sigaclcuni  34302  mbfmfun  34437  dya2icoseg2  34462  bnj66  35042  bnj517  35067  cusgr3cyclex  35364  rellysconn  35479  cvmliftlem15  35526  satffunlem2lem1  35632  r1peuqusdeg1  35871  dfrdg4  36179  brcolinear2  36286  brcolinear  36287  ellines  36380  poimirlem29  38016  volsupnfl  38032  unirep  38081  filbcmb  38107  islshpkrN  39612  ispointN  40234  pmapglbx  40261  rngunsnply  43614  elsetpreimafvbi  47866  cycldlenngric  48419  grtrif1o  48433