Theorem rexlimivw 3159

Description: Weaker version of rexlimiv 3156. (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 485	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3155	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  r19.36v  3190  r19.45v  3196  r19.44v  3197  sbcreu  3829  eliun  4953  reusv3i  5361  elrnmptg  5937  fvelrnb  6927  fvelimab  6939  iinpreima  7050  fmpt  7091  fliftfun  7296  elrnmpo  7532  ovelrn  7572  onuninsuci  7820  fiunlem  7923  releldm2  8024  poxp2  8123  poxp3  8130  orderseqlem  8137  tfrlem4  8349  naddunif  8664  iiner  8771  elixpsn  8919  isfi  8956  card2on  9502  brttrcl  9668  tz9.12lem1  9745  rankwflemb  9751  rankxpsuc  9840  scott0  9844  isnum2  9903  cardiun  9940  cardalephex  10046  dfac5lem4  10082  dfac5lem4OLD  10084  dfac12k  10104  cflim2  10220  cfss  10222  cfslb2n  10225  enfin2i  10278  fin23lem30  10299  itunitc  10378  axdc3lem2  10408  iundom2g  10497  pwcfsdom  10541  cfpwsdom  10542  tskr1om2  10726  genpelv  10958  prlem934  10991  suplem1pr  11010  supexpr  11012  supsrlem  11069  supsr  11070  fimaxre3  12138  iswrd  14528  caurcvgr  15701  caurcvg  15704  caucvg  15706  vdwapval  17009  restsspw  17460  mreunirn  17629  brssc  17847  arwhoma  18078  gexcl3  19627  dvdsr  20407  rhmdvdsr  20554  ellspsn  21067  lspprel  21158  ellspd  21851  iincld  23096  ssnei  23167  neindisj2  23180  neitr  23237  lecldbas  23276  tgcnp  23310  cncnp2  23338  lmmo  23437  is2ndc  23503  fbfinnfr  23898  fbunfip  23926  filunirn  23939  fbflim2  24034  flimcls  24042  hauspwpwf1  24044  flftg  24053  isfcls  24066  fclsbas  24078  isfcf  24091  ustfilxp  24270  ustbas  24284  restutop  24294  ucnima  24337  xmetunirn  24394  metss  24565  metrest  24581  restmetu  24627  qdensere  24826  elpi1  25104  lmmbr  25317  caun0  25340  nulmbl2  25595  itg2l  25788  aannenlem2  26390  taylfval  26419  ulmcl  26441  ulmpm  26443  ulmss  26457  elno  27707  nofun  27710  norn  27712  madeval2  27923  elmade  27947  tglnunirn  28714  ishpg  28929  edglnl  29341  uhgrwkspthlem1  29950  usgr2pth  29961  umgr2wlk  30146  elwwlks2ons3  30152  clwwlknun  30311  frgrncvvdeqlem3  30500  frgr2wwlkn0  30527  frgrreg  30593  hhcms  31403  hhsscms  31478  occllem  31503  occl  31504  chscllem2  31838  r19.29ffa  32668  rabfmpunirn  32852  kerunit  33508  tpr2rico  34206  gsumesum  34353  esumcst  34357  esumfsup  34364  esumpcvgval  34372  esumcvg  34380  sigaclcuni  34412  mbfmfun  34547  dya2icoseg2  34572  bnj66  35152  bnj517  35177  cusgr3cyclex  35483  rellysconn  35598  cvmliftlem15  35645  satffunlem2lem1  35751  r1peuqusdeg1  35990  dfrdg4  36298  brcolinear2  36405  brcolinear  36406  ellines  36499  poimirlem29  38145  volsupnfl  38161  unirep  38210  filbcmb  38236  islshpkrN  39741  ispointN  40363  pmapglbx  40390  rngunsnply  43743  elsetpreimafvbi  47994  cycldlenngric  48547  grtrif1o  48561