Theorem rexlimivw 3151

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  r19.36v  3184  r19.45v  3193  r19.44v  3194  r19.29vvaOLD  3217  sbcreu  3876  eliun  4995  reusv3i  5404  elrnmptg  5972  fvelrnb  6969  fvelimab  6981  iinpreima  7089  fmpt  7130  fliftfun  7332  elrnmpo  7569  ovelrn  7609  onuninsuci  7861  fiunlem  7966  releldm2  8068  poxp2  8168  poxp3  8175  orderseqlem  8182  tfrlem4  8419  naddunif  8731  iiner  8829  elixpsn  8977  isfi  9016  card2on  9594  brttrcl  9753  tz9.12lem1  9827  rankwflemb  9833  rankxpsuc  9922  scott0  9926  isnum2  9985  cardiun  10022  cardalephex  10130  dfac5lem4  10166  dfac5lem4OLD  10168  dfac12k  10188  cflim2  10303  cfss  10305  cfslb2n  10308  enfin2i  10361  fin23lem30  10382  itunitc  10461  axdc3lem2  10491  iundom2g  10580  pwcfsdom  10623  cfpwsdom  10624  tskr1om2  10808  genpelv  11040  prlem934  11073  suplem1pr  11092  supexpr  11094  supsrlem  11151  supsr  11152  fimaxre3  12214  iswrd  14554  caurcvgr  15710  caurcvg  15713  caucvg  15715  vdwapval  17011  restsspw  17476  mreunirn  17644  brssc  17858  arwhoma  18090  gexcl3  19605  dvdsr  20362  rhmdvdsr  20508  ellspsn  21001  lspprel  21093  ellspd  21822  iincld  23047  ssnei  23118  neindisj2  23131  neitr  23188  lecldbas  23227  tgcnp  23261  cncnp2  23289  lmmo  23388  is2ndc  23454  fbfinnfr  23849  fbunfip  23877  filunirn  23890  fbflim2  23985  flimcls  23993  hauspwpwf1  23995  flftg  24004  isfcls  24017  fclsbas  24029  isfcf  24042  ustfilxp  24221  ustbas  24236  restutop  24246  ucnima  24290  xmetunirn  24347  metss  24521  metrest  24537  restmetu  24583  qdensere  24790  elpi1  25078  lmmbr  25292  caun0  25315  nulmbl2  25571  itg2l  25764  aannenlem2  26371  taylfval  26400  ulmcl  26424  ulmpm  26426  ulmss  26440  elno  27690  nofun  27694  norn  27696  madeval2  27892  elmade  27906  tglnunirn  28556  ishpg  28767  edglnl  29160  uhgrwkspthlem1  29773  usgr2pth  29784  umgr2wlk  29969  elwwlks2ons3  29975  clwwlknun  30131  frgrncvvdeqlem3  30320  frgr2wwlkn0  30347  frgrreg  30413  hhcms  31222  hhsscms  31297  occllem  31322  occl  31323  chscllem2  31657  r19.29ffa  32490  rabfmpunirn  32663  kerunit  33349  tpr2rico  33911  gsumesum  34060  esumcst  34064  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  sigaclcuni  34119  mbfmfun  34254  dya2icoseg2  34280  bnj66  34874  bnj517  34899  cusgr3cyclex  35141  rellysconn  35256  cvmliftlem15  35303  satffunlem2lem1  35409  r1peuqusdeg1  35648  dfrdg4  35952  brcolinear2  36059  brcolinear  36060  ellines  36153  poimirlem29  37656  volsupnfl  37672  unirep  37721  filbcmb  37747  islshpkrN  39121  ispointN  39744  pmapglbx  39771  rngunsnply  43181  elsetpreimafvbi  47378  grtrif1o  47909