Theorem rexlimivw 3148

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  r19.36v  3181  r19.45v  3190  r19.44v  3191  r19.29vvaOLD  3214  sbcreu  3884  eliun  4999  reusv3i  5409  elrnmptg  5974  fvelrnb  6968  fvelimab  6980  iinpreima  7088  fmpt  7129  fliftfun  7331  elrnmpo  7568  ovelrn  7608  onuninsuci  7860  fiunlem  7964  releldm2  8066  poxp2  8166  poxp3  8173  orderseqlem  8180  tfrlem4  8417  naddunif  8729  iiner  8827  elixpsn  8975  isfi  9014  card2on  9591  brttrcl  9750  tz9.12lem1  9824  rankwflemb  9830  rankxpsuc  9919  scott0  9923  isnum2  9982  cardiun  10019  cardalephex  10127  dfac5lem4  10163  dfac5lem4OLD  10165  dfac12k  10185  cflim2  10300  cfss  10302  cfslb2n  10305  enfin2i  10358  fin23lem30  10379  itunitc  10458  axdc3lem2  10488  iundom2g  10577  pwcfsdom  10620  cfpwsdom  10621  tskr1om2  10805  genpelv  11037  prlem934  11070  suplem1pr  11089  supexpr  11091  supsrlem  11148  supsr  11149  fimaxre3  12211  iswrd  14550  caurcvgr  15706  caurcvg  15709  caucvg  15711  vdwapval  17006  restsspw  17477  mreunirn  17645  brssc  17861  arwhoma  18098  gexcl3  19619  dvdsr  20378  rhmdvdsr  20524  ellspsn  21018  lspprel  21110  ellspd  21839  iincld  23062  ssnei  23133  neindisj2  23146  neitr  23203  lecldbas  23242  tgcnp  23276  cncnp2  23304  lmmo  23403  is2ndc  23469  fbfinnfr  23864  fbunfip  23892  filunirn  23905  fbflim2  24000  flimcls  24008  hauspwpwf1  24010  flftg  24019  isfcls  24032  fclsbas  24044  isfcf  24057  ustfilxp  24236  ustbas  24251  restutop  24261  ucnima  24305  xmetunirn  24362  metss  24536  metrest  24552  restmetu  24598  qdensere  24805  elpi1  25091  lmmbr  25305  caun0  25328  nulmbl2  25584  itg2l  25778  aannenlem2  26385  taylfval  26414  ulmcl  26438  ulmpm  26440  ulmss  26454  elno  27704  nofun  27708  norn  27710  madeval2  27906  elmade  27920  tglnunirn  28570  ishpg  28781  edglnl  29174  uhgrwkspthlem1  29785  usgr2pth  29796  umgr2wlk  29978  elwwlks2ons3  29984  clwwlknun  30140  frgrncvvdeqlem3  30329  frgr2wwlkn0  30356  frgrreg  30422  hhcms  31231  hhsscms  31306  occllem  31331  occl  31332  chscllem2  31666  r19.29ffa  32499  rabfmpunirn  32669  kerunit  33328  tpr2rico  33872  gsumesum  34039  esumcst  34043  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  sigaclcuni  34098  mbfmfun  34233  dya2icoseg2  34259  bnj66  34852  bnj517  34877  cusgr3cyclex  35120  rellysconn  35235  cvmliftlem15  35282  satffunlem2lem1  35388  r1peuqusdeg1  35627  dfrdg4  35932  brcolinear2  36039  brcolinear  36040  ellines  36133  poimirlem29  37635  volsupnfl  37651  unirep  37700  filbcmb  37726  islshpkrN  39101  ispointN  39724  pmapglbx  39751  rngunsnply  43157  elsetpreimafvbi  47315  grtrif1o  47846