Theorem rexlimivw 3129

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.36v  3160  r19.45v  3166  r19.44v  3167  sbcreu  3822  eliun  4943  reusv3i  5340  elrnmptg  5900  fvelrnb  6882  fvelimab  6894  iinpreima  7002  fmpt  7043  fliftfun  7246  elrnmpo  7482  ovelrn  7522  onuninsuci  7770  fiunlem  7874  releldm2  7975  poxp2  8073  poxp3  8080  orderseqlem  8087  tfrlem4  8298  naddunif  8608  iiner  8713  elixpsn  8861  isfi  8898  card2on  9440  brttrcl  9603  tz9.12lem1  9680  rankwflemb  9686  rankxpsuc  9775  scott0  9779  isnum2  9838  cardiun  9875  cardalephex  9981  dfac5lem4  10017  dfac5lem4OLD  10019  dfac12k  10039  cflim2  10154  cfss  10156  cfslb2n  10159  enfin2i  10212  fin23lem30  10233  itunitc  10312  axdc3lem2  10342  iundom2g  10431  pwcfsdom  10474  cfpwsdom  10475  tskr1om2  10659  genpelv  10891  prlem934  10924  suplem1pr  10943  supexpr  10945  supsrlem  11002  supsr  11003  fimaxre3  12068  iswrd  14422  caurcvgr  15581  caurcvg  15584  caucvg  15586  vdwapval  16885  restsspw  17335  mreunirn  17503  brssc  17721  arwhoma  17952  gexcl3  19499  dvdsr  20280  rhmdvdsr  20423  ellspsn  20936  lspprel  21028  ellspd  21739  iincld  22954  ssnei  23025  neindisj2  23038  neitr  23095  lecldbas  23134  tgcnp  23168  cncnp2  23196  lmmo  23295  is2ndc  23361  fbfinnfr  23756  fbunfip  23784  filunirn  23797  fbflim2  23892  flimcls  23900  hauspwpwf1  23902  flftg  23911  isfcls  23924  fclsbas  23936  isfcf  23949  ustfilxp  24128  ustbas  24142  restutop  24152  ucnima  24195  xmetunirn  24252  metss  24423  metrest  24439  restmetu  24485  qdensere  24684  elpi1  24972  lmmbr  25185  caun0  25208  nulmbl2  25464  itg2l  25657  aannenlem2  26264  taylfval  26293  ulmcl  26317  ulmpm  26319  ulmss  26333  elno  27584  nofun  27588  norn  27590  madeval2  27794  elmade  27812  tglnunirn  28526  ishpg  28737  edglnl  29121  uhgrwkspthlem1  29731  usgr2pth  29742  umgr2wlk  29927  elwwlks2ons3  29933  clwwlknun  30092  frgrncvvdeqlem3  30281  frgr2wwlkn0  30308  frgrreg  30374  hhcms  31183  hhsscms  31258  occllem  31283  occl  31284  chscllem2  31618  r19.29ffa  32450  rabfmpunirn  32635  kerunit  33290  tpr2rico  33925  gsumesum  34072  esumcst  34076  esumfsup  34083  esumpcvgval  34091  esumcvg  34099  sigaclcuni  34131  mbfmfun  34266  dya2icoseg2  34291  bnj66  34872  bnj517  34897  cusgr3cyclex  35180  rellysconn  35295  cvmliftlem15  35342  satffunlem2lem1  35448  r1peuqusdeg1  35687  dfrdg4  35993  brcolinear2  36100  brcolinear  36101  ellines  36194  poimirlem29  37697  volsupnfl  37713  unirep  37762  filbcmb  37788  islshpkrN  39167  ispointN  39789  pmapglbx  39816  rngunsnply  43210  elsetpreimafvbi  47430  cycldlenngric  47967  grtrif1o  47981