Theorem rexlimivw 3162

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  r19.36v  3193  r19.45v  3199  r19.44v  3200  sbcreu  3829  eliun  4960  reusv3i  5375  elrnmptg  5951  fvelrnb  6941  fvelimab  6953  iinpreima  7064  fmpt  7105  fliftfun  7310  elrnmpo  7546  ovelrn  7586  onuninsuci  7832  fiunlem  7935  releldm2  8036  poxp2  8135  poxp3  8142  orderseqlem  8149  tfrlem4  8361  naddunif  8676  iiner  8783  elixpsn  8931  isfi  8968  card2on  9512  brttrcl  9678  tz9.12lem1  9755  rankwflemb  9761  rankxpsuc  9850  scott0  9856  isnum2  9927  cardiun  9964  cardalephex  10070  dfac5lem4  10106  dfac12k  10127  cflim2  10242  cfss  10244  cfslb2n  10247  enfin2i  10300  fin23lem30  10321  itunitc  10400  axdc3lem2  10430  iundom2g  10519  pwcfsdom  10563  cfpwsdom  10564  tskr1om2  10748  genpelv  10980  prlem934  11013  suplem1pr  11032  supexpr  11034  supsrlem  11091  supsr  11092  fimaxre3  12156  iswrd  14548  caurcvgr  15721  caurcvg  15724  caucvg  15726  vdwapval  17028  restsspw  17479  mreunirn  17648  brssc  17866  arwhoma  18097  gexcl3  19652  dvdsr  20440  rhmdvdsr  20605  ellspsn  21124  lspprel  21215  ellspd  21952  iincld  23196  ssnei  23267  neindisj2  23280  neitr  23337  lecldbas  23376  tgcnp  23410  cncnp2  23438  lmmo  23537  is2ndc  23603  fbfinnfr  23998  fbunfip  24026  filunirn  24039  fbflim2  24134  flimcls  24142  hauspwpwf1  24144  flftg  24153  isfcls  24166  fclsbas  24178  isfcf  24191  ustfilxp  24370  ustbas  24384  restutop  24394  ucnima  24437  xmetunirn  24494  metss  24665  metrest  24681  restmetu  24727  qdensere  24926  elpi1  25204  lmmbr  25417  caun0  25440  nulmbl2  25695  itg2l  25888  aannenlem2  26492  taylfval  26522  ulmcl  26544  ulmpm  26546  ulmss  26560  elno  27810  nofun  27813  norn  27815  madeval2  28026  elmade  28050  tglnunirn  28817  ishpg  29041  edglnl  29493  uhgrwkspthlem1  30102  usgr2pth  30113  umgr2wlk  30298  elwwlks2ons3  30304  clwwlknun  30463  frgrncvvdeqlem3  30652  frgr2wwlkn0  30679  frgrreg  30745  hhcms  31555  hhsscms  31630  occllem  31655  occl  31656  chscllem2  31990  r19.29ffa  32818  rabfmpunirn  32998  kerunit  33645  tpr2rico  34302  gsumesum  34449  esumcst  34453  esumfsup  34460  esumpcvgval  34468  esumcvg  34476  sigaclcuni  34508  mbfmfun  34643  dya2icoseg2  34668  bnj66  35248  bnj517  35273  cusgr3cyclex  35628  rellysconn  35743  cvmliftlem15  35790  satffunlem2lem1  35896  r1peuqusdeg1  36135  dfrdg4  36443  brcolinear2  36550  brcolinear  36551  ellines  36644  poimirlem29  38300  volsupnfl  38316  unirep  38365  filbcmb  38391  islshpkrN  39894  ispointN  40516  pmapglbx  40543  rngunsnply  43896  elsetpreimafvbi  48140  cycldlenngric  48693  grtrif1o  48707