Theorem rexlimivw 3135

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.36v  3166  r19.45v  3172  r19.44v  3173  sbcreu  3828  eliun  4952  reusv3i  5351  elrnmptg  5918  fvelrnb  6902  fvelimab  6914  iinpreima  7023  fmpt  7064  fliftfun  7268  elrnmpo  7504  ovelrn  7544  onuninsuci  7792  fiunlem  7896  releldm2  7997  poxp2  8095  poxp3  8102  orderseqlem  8109  tfrlem4  8320  naddunif  8631  iiner  8738  elixpsn  8887  isfi  8924  card2on  9471  brttrcl  9634  tz9.12lem1  9711  rankwflemb  9717  rankxpsuc  9806  scott0  9810  isnum2  9869  cardiun  9906  cardalephex  10012  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12k  10070  cflim2  10185  cfss  10187  cfslb2n  10190  enfin2i  10243  fin23lem30  10264  itunitc  10343  axdc3lem2  10373  iundom2g  10462  pwcfsdom  10506  cfpwsdom  10507  tskr1om2  10691  genpelv  10923  prlem934  10956  suplem1pr  10975  supexpr  10977  supsrlem  11034  supsr  11035  fimaxre3  12100  iswrd  14450  caurcvgr  15609  caurcvg  15612  caucvg  15614  vdwapval  16913  restsspw  17363  mreunirn  17532  brssc  17750  arwhoma  17981  gexcl3  19528  dvdsr  20310  rhmdvdsr  20453  ellspsn  20966  lspprel  21058  ellspd  21769  iincld  22995  ssnei  23066  neindisj2  23079  neitr  23136  lecldbas  23175  tgcnp  23209  cncnp2  23237  lmmo  23336  is2ndc  23402  fbfinnfr  23797  fbunfip  23825  filunirn  23838  fbflim2  23933  flimcls  23941  hauspwpwf1  23943  flftg  23952  isfcls  23965  fclsbas  23977  isfcf  23990  ustfilxp  24169  ustbas  24183  restutop  24193  ucnima  24236  xmetunirn  24293  metss  24464  metrest  24480  restmetu  24526  qdensere  24725  elpi1  25013  lmmbr  25226  caun0  25249  nulmbl2  25505  itg2l  25698  aannenlem2  26305  taylfval  26334  ulmcl  26358  ulmpm  26360  ulmss  26374  elno  27625  nofun  27629  norn  27631  madeval2  27841  elmade  27865  tglnunirn  28632  ishpg  28843  edglnl  29228  uhgrwkspthlem1  29838  usgr2pth  29849  umgr2wlk  30034  elwwlks2ons3  30040  clwwlknun  30199  frgrncvvdeqlem3  30388  frgr2wwlkn0  30415  frgrreg  30481  hhcms  31291  hhsscms  31366  occllem  31391  occl  31392  chscllem2  31726  r19.29ffa  32557  rabfmpunirn  32743  kerunit  33418  tpr2rico  34090  gsumesum  34237  esumcst  34241  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  sigaclcuni  34296  mbfmfun  34431  dya2icoseg2  34456  bnj66  35036  bnj517  35061  cusgr3cyclex  35352  rellysconn  35467  cvmliftlem15  35514  satffunlem2lem1  35620  r1peuqusdeg1  35859  dfrdg4  36167  brcolinear2  36274  brcolinear  36275  ellines  36368  poimirlem29  37900  volsupnfl  37916  unirep  37965  filbcmb  37991  islshpkrN  39496  ispointN  40118  pmapglbx  40145  rngunsnply  43526  elsetpreimafvbi  47751  cycldlenngric  48288  grtrif1o  48302