Theorem rexlimivw 3133

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3060

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 3061

This theorem is referenced by:  r19.36v  3164  r19.45v  3170  r19.44v  3171  sbcreu  3826  eliun  4950  reusv3i  5349  elrnmptg  5910  fvelrnb  6894  fvelimab  6906  iinpreima  7014  fmpt  7055  fliftfun  7258  elrnmpo  7494  ovelrn  7534  onuninsuci  7782  fiunlem  7886  releldm2  7987  poxp2  8085  poxp3  8092  orderseqlem  8099  tfrlem4  8310  naddunif  8621  iiner  8726  elixpsn  8875  isfi  8912  card2on  9459  brttrcl  9622  tz9.12lem1  9699  rankwflemb  9705  rankxpsuc  9794  scott0  9798  isnum2  9857  cardiun  9894  cardalephex  10000  dfac5lem4  10036  dfac5lem4OLD  10038  dfac12k  10058  cflim2  10173  cfss  10175  cfslb2n  10178  enfin2i  10231  fin23lem30  10252  itunitc  10331  axdc3lem2  10361  iundom2g  10450  pwcfsdom  10494  cfpwsdom  10495  tskr1om2  10679  genpelv  10911  prlem934  10944  suplem1pr  10963  supexpr  10965  supsrlem  11022  supsr  11023  fimaxre3  12088  iswrd  14438  caurcvgr  15597  caurcvg  15600  caucvg  15602  vdwapval  16901  restsspw  17351  mreunirn  17520  brssc  17738  arwhoma  17969  gexcl3  19516  dvdsr  20298  rhmdvdsr  20441  ellspsn  20954  lspprel  21046  ellspd  21757  iincld  22983  ssnei  23054  neindisj2  23067  neitr  23124  lecldbas  23163  tgcnp  23197  cncnp2  23225  lmmo  23324  is2ndc  23390  fbfinnfr  23785  fbunfip  23813  filunirn  23826  fbflim2  23921  flimcls  23929  hauspwpwf1  23931  flftg  23940  isfcls  23953  fclsbas  23965  isfcf  23978  ustfilxp  24157  ustbas  24171  restutop  24181  ucnima  24224  xmetunirn  24281  metss  24452  metrest  24468  restmetu  24514  qdensere  24713  elpi1  25001  lmmbr  25214  caun0  25237  nulmbl2  25493  itg2l  25686  aannenlem2  26293  taylfval  26322  ulmcl  26346  ulmpm  26348  ulmss  26362  elno  27613  nofun  27617  norn  27619  madeval2  27829  elmade  27853  tglnunirn  28620  ishpg  28831  edglnl  29216  uhgrwkspthlem1  29826  usgr2pth  29837  umgr2wlk  30022  elwwlks2ons3  30028  clwwlknun  30187  frgrncvvdeqlem3  30376  frgr2wwlkn0  30403  frgrreg  30469  hhcms  31278  hhsscms  31353  occllem  31378  occl  31379  chscllem2  31713  r19.29ffa  32545  rabfmpunirn  32731  kerunit  33406  tpr2rico  34069  gsumesum  34216  esumcst  34220  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  sigaclcuni  34275  mbfmfun  34410  dya2icoseg2  34435  bnj66  35016  bnj517  35041  cusgr3cyclex  35330  rellysconn  35445  cvmliftlem15  35492  satffunlem2lem1  35598  r1peuqusdeg1  35837  dfrdg4  36145  brcolinear2  36252  brcolinear  36253  ellines  36346  poimirlem29  37850  volsupnfl  37866  unirep  37915  filbcmb  37941  islshpkrN  39380  ispointN  40002  pmapglbx  40029  rngunsnply  43411  elsetpreimafvbi  47637  cycldlenngric  48174  grtrif1o  48188