Theorem rexlimivw 3130

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  r19.36v  3162  r19.45v  3171  r19.44v  3172  sbcreu  3839  eliun  4959  reusv3i  5359  elrnmptg  5925  fvelrnb  6921  fvelimab  6933  iinpreima  7041  fmpt  7082  fliftfun  7287  elrnmpo  7525  ovelrn  7565  onuninsuci  7816  fiunlem  7920  releldm2  8022  poxp2  8122  poxp3  8129  orderseqlem  8136  tfrlem4  8347  naddunif  8657  iiner  8762  elixpsn  8910  isfi  8947  card2on  9507  brttrcl  9666  tz9.12lem1  9740  rankwflemb  9746  rankxpsuc  9835  scott0  9839  isnum2  9898  cardiun  9935  cardalephex  10043  dfac5lem4  10079  dfac5lem4OLD  10081  dfac12k  10101  cflim2  10216  cfss  10218  cfslb2n  10221  enfin2i  10274  fin23lem30  10295  itunitc  10374  axdc3lem2  10404  iundom2g  10493  pwcfsdom  10536  cfpwsdom  10537  tskr1om2  10721  genpelv  10953  prlem934  10986  suplem1pr  11005  supexpr  11007  supsrlem  11064  supsr  11065  fimaxre3  12129  iswrd  14480  caurcvgr  15640  caurcvg  15643  caucvg  15645  vdwapval  16944  restsspw  17394  mreunirn  17562  brssc  17776  arwhoma  18007  gexcl3  19517  dvdsr  20271  rhmdvdsr  20417  ellspsn  20909  lspprel  21001  ellspd  21711  iincld  22926  ssnei  22997  neindisj2  23010  neitr  23067  lecldbas  23106  tgcnp  23140  cncnp2  23168  lmmo  23267  is2ndc  23333  fbfinnfr  23728  fbunfip  23756  filunirn  23769  fbflim2  23864  flimcls  23872  hauspwpwf1  23874  flftg  23883  isfcls  23896  fclsbas  23908  isfcf  23921  ustfilxp  24100  ustbas  24115  restutop  24125  ucnima  24168  xmetunirn  24225  metss  24396  metrest  24412  restmetu  24458  qdensere  24657  elpi1  24945  lmmbr  25158  caun0  25181  nulmbl2  25437  itg2l  25630  aannenlem2  26237  taylfval  26266  ulmcl  26290  ulmpm  26292  ulmss  26306  elno  27557  nofun  27561  norn  27563  madeval2  27761  elmade  27779  tglnunirn  28475  ishpg  28686  edglnl  29070  uhgrwkspthlem1  29683  usgr2pth  29694  umgr2wlk  29879  elwwlks2ons3  29885  clwwlknun  30041  frgrncvvdeqlem3  30230  frgr2wwlkn0  30257  frgrreg  30323  hhcms  31132  hhsscms  31207  occllem  31232  occl  31233  chscllem2  31567  r19.29ffa  32400  rabfmpunirn  32577  kerunit  33297  tpr2rico  33902  gsumesum  34049  esumcst  34053  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  sigaclcuni  34108  mbfmfun  34243  dya2icoseg2  34269  bnj66  34850  bnj517  34875  cusgr3cyclex  35123  rellysconn  35238  cvmliftlem15  35285  satffunlem2lem1  35391  r1peuqusdeg1  35630  dfrdg4  35939  brcolinear2  36046  brcolinear  36047  ellines  36140  poimirlem29  37643  volsupnfl  37659  unirep  37708  filbcmb  37734  islshpkrN  39113  ispointN  39736  pmapglbx  39763  rngunsnply  43158  elsetpreimafvbi  47392  cycldlenngric  47928  grtrif1o  47941