Theorem rexlimivw 3157

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  r19.36v  3190  r19.45v  3199  r19.44v  3200  r19.29vvaOLD  3223  sbcreu  3898  eliun  5019  reusv3i  5422  elrnmptg  5984  fvelrnb  6982  fvelimab  6994  iinpreima  7102  fmpt  7144  fliftfun  7348  elrnmpo  7586  ovelrn  7626  onuninsuci  7877  fiunlem  7982  releldm2  8084  poxp2  8184  poxp3  8191  orderseqlem  8198  tfrlem4  8435  naddunif  8749  iiner  8847  elixpsn  8995  isfi  9036  card2on  9623  brttrcl  9782  tz9.12lem1  9856  rankwflemb  9862  rankxpsuc  9951  scott0  9955  isnum2  10014  cardiun  10051  cardalephex  10159  dfac5lem4  10195  dfac5lem4OLD  10197  dfac12k  10217  cflim2  10332  cfss  10334  cfslb2n  10337  enfin2i  10390  fin23lem30  10411  itunitc  10490  axdc3lem2  10520  iundom2g  10609  pwcfsdom  10652  cfpwsdom  10653  tskr1om2  10837  genpelv  11069  prlem934  11102  suplem1pr  11121  supexpr  11123  supsrlem  11180  supsr  11181  fimaxre3  12241  iswrd  14564  caurcvgr  15722  caurcvg  15725  caucvg  15727  vdwapval  17020  restsspw  17491  mreunirn  17659  brssc  17875  arwhoma  18112  gexcl3  19629  dvdsr  20388  rhmdvdsr  20534  ellspsn  21024  lspprel  21116  ellspd  21845  iincld  23068  ssnei  23139  neindisj2  23152  neitr  23209  lecldbas  23248  tgcnp  23282  cncnp2  23310  lmmo  23409  is2ndc  23475  fbfinnfr  23870  fbunfip  23898  filunirn  23911  fbflim2  24006  flimcls  24014  hauspwpwf1  24016  flftg  24025  isfcls  24038  fclsbas  24050  isfcf  24063  ustfilxp  24242  ustbas  24257  restutop  24267  ucnima  24311  xmetunirn  24368  metss  24542  metrest  24558  restmetu  24604  qdensere  24811  elpi1  25097  lmmbr  25311  caun0  25334  nulmbl2  25590  itg2l  25784  aannenlem2  26389  taylfval  26418  ulmcl  26442  ulmpm  26444  ulmss  26458  elno  27708  nofun  27712  norn  27714  madeval2  27910  elmade  27924  tglnunirn  28574  ishpg  28785  edglnl  29178  uhgrwkspthlem1  29789  usgr2pth  29800  umgr2wlk  29982  elwwlks2ons3  29988  clwwlknun  30144  frgrncvvdeqlem3  30333  frgr2wwlkn0  30360  frgrreg  30426  hhcms  31235  hhsscms  31310  occllem  31335  occl  31336  chscllem2  31670  r19.29ffa  32500  rabfmpunirn  32671  kerunit  33314  tpr2rico  33858  gsumesum  34023  esumcst  34027  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  sigaclcuni  34082  mbfmfun  34217  dya2icoseg2  34243  bnj66  34836  bnj517  34861  cusgr3cyclex  35104  rellysconn  35219  cvmliftlem15  35266  satffunlem2lem1  35372  r1peuqusdeg1  35611  dfrdg4  35915  brcolinear2  36022  brcolinear  36023  ellines  36116  poimirlem29  37609  volsupnfl  37625  unirep  37674  filbcmb  37700  islshpkrN  39076  ispointN  39699  pmapglbx  39726  rngunsnply  43130  elsetpreimafvbi  47265  grtrif1o  47793