Theorem rexlimivw 3131

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

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

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 3059

This theorem is referenced by:  r19.36v  3162  r19.45v  3168  r19.44v  3169  sbcreu  3824  eliun  4948  reusv3i  5347  elrnmptg  5908  fvelrnb  6892  fvelimab  6904  iinpreima  7012  fmpt  7053  fliftfun  7256  elrnmpo  7492  ovelrn  7532  onuninsuci  7780  fiunlem  7884  releldm2  7985  poxp2  8083  poxp3  8090  orderseqlem  8097  tfrlem4  8308  naddunif  8619  iiner  8724  elixpsn  8873  isfi  8910  card2on  9457  brttrcl  9620  tz9.12lem1  9697  rankwflemb  9703  rankxpsuc  9792  scott0  9796  isnum2  9855  cardiun  9892  cardalephex  9998  dfac5lem4  10034  dfac5lem4OLD  10036  dfac12k  10056  cflim2  10171  cfss  10173  cfslb2n  10176  enfin2i  10229  fin23lem30  10250  itunitc  10329  axdc3lem2  10359  iundom2g  10448  pwcfsdom  10492  cfpwsdom  10493  tskr1om2  10677  genpelv  10909  prlem934  10942  suplem1pr  10961  supexpr  10963  supsrlem  11020  supsr  11021  fimaxre3  12086  iswrd  14436  caurcvgr  15595  caurcvg  15598  caucvg  15600  vdwapval  16899  restsspw  17349  mreunirn  17518  brssc  17736  arwhoma  17967  gexcl3  19514  dvdsr  20296  rhmdvdsr  20439  ellspsn  20952  lspprel  21044  ellspd  21755  iincld  22981  ssnei  23052  neindisj2  23065  neitr  23122  lecldbas  23161  tgcnp  23195  cncnp2  23223  lmmo  23322  is2ndc  23388  fbfinnfr  23783  fbunfip  23811  filunirn  23824  fbflim2  23919  flimcls  23927  hauspwpwf1  23929  flftg  23938  isfcls  23951  fclsbas  23963  isfcf  23976  ustfilxp  24155  ustbas  24169  restutop  24179  ucnima  24222  xmetunirn  24279  metss  24450  metrest  24466  restmetu  24512  qdensere  24711  elpi1  24999  lmmbr  25212  caun0  25235  nulmbl2  25491  itg2l  25684  aannenlem2  26291  taylfval  26320  ulmcl  26344  ulmpm  26346  ulmss  26360  elno  27611  nofun  27615  norn  27617  madeval2  27821  elmade  27839  tglnunirn  28569  ishpg  28780  edglnl  29165  uhgrwkspthlem1  29775  usgr2pth  29786  umgr2wlk  29971  elwwlks2ons3  29977  clwwlknun  30136  frgrncvvdeqlem3  30325  frgr2wwlkn0  30352  frgrreg  30418  hhcms  31227  hhsscms  31302  occllem  31327  occl  31328  chscllem2  31662  r19.29ffa  32494  rabfmpunirn  32680  kerunit  33355  tpr2rico  34018  gsumesum  34165  esumcst  34169  esumfsup  34176  esumpcvgval  34184  esumcvg  34192  sigaclcuni  34224  mbfmfun  34359  dya2icoseg2  34384  bnj66  34965  bnj517  34990  cusgr3cyclex  35279  rellysconn  35394  cvmliftlem15  35441  satffunlem2lem1  35547  r1peuqusdeg1  35786  dfrdg4  36094  brcolinear2  36201  brcolinear  36202  ellines  36295  poimirlem29  37789  volsupnfl  37805  unirep  37854  filbcmb  37880  islshpkrN  39319  ispointN  39941  pmapglbx  39968  rngunsnply  43353  elsetpreimafvbi  47579  cycldlenngric  48116  grtrif1o  48130