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  3161  r19.45v  3169  r19.44v  3170  sbcreu  3836  eliun  4955  reusv3i  5354  elrnmptg  5914  fvelrnb  6903  fvelimab  6915  iinpreima  7023  fmpt  7064  fliftfun  7269  elrnmpo  7505  ovelrn  7545  onuninsuci  7796  fiunlem  7900  releldm2  8001  poxp2  8099  poxp3  8106  orderseqlem  8113  tfrlem4  8324  naddunif  8634  iiner  8739  elixpsn  8887  isfi  8924  card2on  9483  brttrcl  9642  tz9.12lem1  9716  rankwflemb  9722  rankxpsuc  9811  scott0  9815  isnum2  9874  cardiun  9911  cardalephex  10019  dfac5lem4  10055  dfac5lem4OLD  10057  dfac12k  10077  cflim2  10192  cfss  10194  cfslb2n  10197  enfin2i  10250  fin23lem30  10271  itunitc  10350  axdc3lem2  10380  iundom2g  10469  pwcfsdom  10512  cfpwsdom  10513  tskr1om2  10697  genpelv  10929  prlem934  10962  suplem1pr  10981  supexpr  10983  supsrlem  11040  supsr  11041  fimaxre3  12105  iswrd  14456  caurcvgr  15616  caurcvg  15619  caucvg  15621  vdwapval  16920  restsspw  17370  mreunirn  17538  brssc  17752  arwhoma  17983  gexcl3  19493  dvdsr  20247  rhmdvdsr  20393  ellspsn  20885  lspprel  20977  ellspd  21687  iincld  22902  ssnei  22973  neindisj2  22986  neitr  23043  lecldbas  23082  tgcnp  23116  cncnp2  23144  lmmo  23243  is2ndc  23309  fbfinnfr  23704  fbunfip  23732  filunirn  23745  fbflim2  23840  flimcls  23848  hauspwpwf1  23850  flftg  23859  isfcls  23872  fclsbas  23884  isfcf  23897  ustfilxp  24076  ustbas  24091  restutop  24101  ucnima  24144  xmetunirn  24201  metss  24372  metrest  24388  restmetu  24434  qdensere  24633  elpi1  24921  lmmbr  25134  caun0  25157  nulmbl2  25413  itg2l  25606  aannenlem2  26213  taylfval  26242  ulmcl  26266  ulmpm  26268  ulmss  26282  elno  27533  nofun  27537  norn  27539  madeval2  27737  elmade  27755  tglnunirn  28451  ishpg  28662  edglnl  29046  uhgrwkspthlem1  29656  usgr2pth  29667  umgr2wlk  29852  elwwlks2ons3  29858  clwwlknun  30014  frgrncvvdeqlem3  30203  frgr2wwlkn0  30230  frgrreg  30296  hhcms  31105  hhsscms  31180  occllem  31205  occl  31206  chscllem2  31540  r19.29ffa  32373  rabfmpunirn  32550  kerunit  33270  tpr2rico  33875  gsumesum  34022  esumcst  34026  esumfsup  34033  esumpcvgval  34041  esumcvg  34049  sigaclcuni  34081  mbfmfun  34216  dya2icoseg2  34242  bnj66  34823  bnj517  34848  cusgr3cyclex  35096  rellysconn  35211  cvmliftlem15  35258  satffunlem2lem1  35364  r1peuqusdeg1  35603  dfrdg4  35912  brcolinear2  36019  brcolinear  36020  ellines  36113  poimirlem29  37616  volsupnfl  37632  unirep  37681  filbcmb  37707  islshpkrN  39086  ispointN  39709  pmapglbx  39736  rngunsnply  43131  elsetpreimafvbi  47365  cycldlenngric  47901  grtrif1o  47914