Theorem rexlimivw 3131

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  r19.36v  3163  r19.45v  3172  r19.44v  3173  sbcreu  3842  eliun  4962  reusv3i  5362  elrnmptg  5928  fvelrnb  6924  fvelimab  6936  iinpreima  7044  fmpt  7085  fliftfun  7290  elrnmpo  7528  ovelrn  7568  onuninsuci  7819  fiunlem  7923  releldm2  8025  poxp2  8125  poxp3  8132  orderseqlem  8139  tfrlem4  8350  naddunif  8660  iiner  8765  elixpsn  8913  isfi  8950  card2on  9514  brttrcl  9673  tz9.12lem1  9747  rankwflemb  9753  rankxpsuc  9842  scott0  9846  isnum2  9905  cardiun  9942  cardalephex  10050  dfac5lem4  10086  dfac5lem4OLD  10088  dfac12k  10108  cflim2  10223  cfss  10225  cfslb2n  10228  enfin2i  10281  fin23lem30  10302  itunitc  10381  axdc3lem2  10411  iundom2g  10500  pwcfsdom  10543  cfpwsdom  10544  tskr1om2  10728  genpelv  10960  prlem934  10993  suplem1pr  11012  supexpr  11014  supsrlem  11071  supsr  11072  fimaxre3  12136  iswrd  14487  caurcvgr  15647  caurcvg  15650  caucvg  15652  vdwapval  16951  restsspw  17401  mreunirn  17569  brssc  17783  arwhoma  18014  gexcl3  19524  dvdsr  20278  rhmdvdsr  20424  ellspsn  20916  lspprel  21008  ellspd  21718  iincld  22933  ssnei  23004  neindisj2  23017  neitr  23074  lecldbas  23113  tgcnp  23147  cncnp2  23175  lmmo  23274  is2ndc  23340  fbfinnfr  23735  fbunfip  23763  filunirn  23776  fbflim2  23871  flimcls  23879  hauspwpwf1  23881  flftg  23890  isfcls  23903  fclsbas  23915  isfcf  23928  ustfilxp  24107  ustbas  24122  restutop  24132  ucnima  24175  xmetunirn  24232  metss  24403  metrest  24419  restmetu  24465  qdensere  24664  elpi1  24952  lmmbr  25165  caun0  25188  nulmbl2  25444  itg2l  25637  aannenlem2  26244  taylfval  26273  ulmcl  26297  ulmpm  26299  ulmss  26313  elno  27564  nofun  27568  norn  27570  madeval2  27768  elmade  27786  tglnunirn  28482  ishpg  28693  edglnl  29077  uhgrwkspthlem1  29690  usgr2pth  29701  umgr2wlk  29886  elwwlks2ons3  29892  clwwlknun  30048  frgrncvvdeqlem3  30237  frgr2wwlkn0  30264  frgrreg  30330  hhcms  31139  hhsscms  31214  occllem  31239  occl  31240  chscllem2  31574  r19.29ffa  32407  rabfmpunirn  32584  kerunit  33304  tpr2rico  33909  gsumesum  34056  esumcst  34060  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  sigaclcuni  34115  mbfmfun  34250  dya2icoseg2  34276  bnj66  34857  bnj517  34882  cusgr3cyclex  35130  rellysconn  35245  cvmliftlem15  35292  satffunlem2lem1  35398  r1peuqusdeg1  35637  dfrdg4  35946  brcolinear2  36053  brcolinear  36054  ellines  36147  poimirlem29  37650  volsupnfl  37666  unirep  37715  filbcmb  37741  islshpkrN  39120  ispointN  39743  pmapglbx  39770  rngunsnply  43165  elsetpreimafvbi  47396  cycldlenngric  47932  grtrif1o  47945