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  3815  eliun  4938  reusv3i  5342  elrnmptg  5911  fvelrnb  6895  fvelimab  6907  iinpreima  7016  fmpt  7057  fliftfun  7261  elrnmpo  7497  ovelrn  7537  onuninsuci  7785  fiunlem  7889  releldm2  7990  poxp2  8087  poxp3  8094  orderseqlem  8101  tfrlem4  8312  naddunif  8623  iiner  8730  elixpsn  8879  isfi  8916  card2on  9463  brttrcl  9628  tz9.12lem1  9705  rankwflemb  9711  rankxpsuc  9800  scott0  9804  isnum2  9863  cardiun  9900  cardalephex  10006  dfac5lem4  10042  dfac5lem4OLD  10044  dfac12k  10064  cflim2  10179  cfss  10181  cfslb2n  10184  enfin2i  10237  fin23lem30  10258  itunitc  10337  axdc3lem2  10367  iundom2g  10456  pwcfsdom  10500  cfpwsdom  10501  tskr1om2  10685  genpelv  10917  prlem934  10950  suplem1pr  10969  supexpr  10971  supsrlem  11028  supsr  11029  fimaxre3  12096  iswrd  14471  caurcvgr  15630  caurcvg  15633  caucvg  15635  vdwapval  16938  restsspw  17388  mreunirn  17557  brssc  17775  arwhoma  18006  gexcl3  19556  dvdsr  20336  rhmdvdsr  20479  ellspsn  20992  lspprel  21084  ellspd  21795  iincld  23017  ssnei  23088  neindisj2  23101  neitr  23158  lecldbas  23197  tgcnp  23231  cncnp2  23259  lmmo  23358  is2ndc  23424  fbfinnfr  23819  fbunfip  23847  filunirn  23860  fbflim2  23955  flimcls  23963  hauspwpwf1  23965  flftg  23974  isfcls  23987  fclsbas  23999  isfcf  24012  ustfilxp  24191  ustbas  24205  restutop  24215  ucnima  24258  xmetunirn  24315  metss  24486  metrest  24502  restmetu  24548  qdensere  24747  elpi1  25025  lmmbr  25238  caun0  25261  nulmbl2  25516  itg2l  25709  aannenlem2  26309  taylfval  26338  ulmcl  26362  ulmpm  26364  ulmss  26378  elno  27626  nofun  27630  norn  27632  madeval2  27842  elmade  27866  tglnunirn  28633  ishpg  28844  edglnl  29229  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  32744  kerunit  33403  tpr2rico  34075  gsumesum  34222  esumcst  34226  esumfsup  34233  esumpcvgval  34241  esumcvg  34249  sigaclcuni  34281  mbfmfun  34416  dya2icoseg2  34441  bnj66  35021  bnj517  35046  cusgr3cyclex  35337  rellysconn  35452  cvmliftlem15  35499  satffunlem2lem1  35605  r1peuqusdeg1  35844  dfrdg4  36152  brcolinear2  36259  brcolinear  36260  ellines  36353  poimirlem29  37987  volsupnfl  38003  unirep  38052  filbcmb  38078  islshpkrN  39583  ispointN  40205  pmapglbx  40232  rngunsnply  43618  elsetpreimafvbi  47866  cycldlenngric  48419  grtrif1o  48433