Theorem rexlimivw 3284

Description: Weaker version of rexlimiv 3282. (Contributed by FL, 19-Sep-2011.)

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	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 3282	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3141

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 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  r19.29vva  3338  r19.29vvaOLD  3339  r19.36v  3344  r19.44v  3354  r19.45v  3355  sbcreu  3861  eliun  4925  reusv3i  5307  elrnmptg  5833  fvelrnb  6728  fvelimab  6739  iinpreima  6839  fmpt  6876  fliftfun  7067  elrnmpo  7289  ovelrn  7326  onuninsuci  7557  fiunlem  7645  releldm2  7744  tfrlem4  8017  iiner  8371  elixpsn  8503  isfi  8535  card2on  9020  tz9.12lem1  9218  rankwflemb  9224  rankxpsuc  9313  scott0  9317  isnum2  9376  cardiun  9413  cardalephex  9518  dfac5lem4  9554  dfac12k  9575  cflim2  9687  cfss  9689  cfslb2n  9692  enfin2i  9745  fin23lem30  9766  itunitc  9845  axdc3lem2  9875  iundom2g  9964  pwcfsdom  10007  cfpwsdom  10008  tskr1om2  10192  genpelv  10424  prlem934  10457  suplem1pr  10476  supexpr  10478  supsrlem  10535  supsr  10536  fimaxre3  11589  iswrd  13866  caurcvgr  15032  caurcvg  15035  caucvg  15037  vdwapval  16311  restsspw  16707  mreunirn  16874  brssc  17086  arwhoma  17307  gexcl3  18714  dvdsr  19398  lspsnel  19777  lspprel  19868  ellspd  20948  iincld  21649  ssnei  21720  neindisj2  21733  neitr  21790  lecldbas  21829  tgcnp  21863  cncnp2  21891  lmmo  21990  is2ndc  22056  fbfinnfr  22451  fbunfip  22479  filunirn  22492  fbflim2  22587  flimcls  22595  hauspwpwf1  22597  flftg  22606  isfcls  22619  fclsbas  22631  isfcf  22644  ustfilxp  22823  ustbas  22838  restutop  22848  ucnima  22892  xmetunirn  22949  metss  23120  metrest  23136  restmetu  23182  qdensere  23380  elpi1  23651  lmmbr  23863  caun0  23886  nulmbl2  24139  itg2l  24332  aannenlem2  24920  taylfval  24949  ulmcl  24971  ulmpm  24973  ulmss  24987  tglnunirn  26336  ishpg  26547  edglnl  26930  uhgrwkspthlem1  27536  usgr2pth  27547  umgr2wlk  27730  elwwlks2ons3  27736  clwwlknun  27893  frgrncvvdeqlem3  28082  frgr2wwlkn0  28109  frgrreg  28175  hhcms  28982  hhsscms  29057  occllem  29082  occl  29083  chscllem2  29417  r19.29ffa  30239  rabfmpunirn  30400  rhmdvdsr  30893  kerunit  30898  tpr2rico  31157  gsumesum  31320  esumcst  31324  esumfsup  31331  esumpcvgval  31339  esumcvg  31347  sigaclcuni  31379  mbfmfun  31514  dya2icoseg2  31538  bnj66  32134  bnj517  32159  cusgr3cyclex  32385  rellysconn  32500  cvmliftlem15  32547  satffunlem2lem1  32653  orderseqlem  33096  nofun  33158  norn  33160  madeval2  33292  dfrdg4  33414  brcolinear2  33521  brcolinear  33522  ellines  33615  poimirlem29  34923  volsupnfl  34939  unirep  34990  filbcmb  35017  islshpkrN  36258  ispointN  36880  pmapglbx  36907  rngunsnply  39780  elsetpreimafvbi  43558