Theorem rexlimivw 3207

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

Syntax hints:   → wi 4   ∈ wcel 2112  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077

This theorem is referenced by:  r19.29vva  3258  r19.36v  3262  r19.44v  3271  r19.45v  3272  sbcreu  3783  eliun  4885  reusv3i  5271  elrnmptg  5798  fvelrnb  6712  fvelimab  6723  iinpreima  6826  fmpt  6863  fliftfun  7057  elrnmpo  7280  ovelrn  7318  onuninsuci  7552  fiunlem  7645  releldm2  7744  tfrlem4  8023  iiner  8377  elixpsn  8517  isfi  8549  card2on  9041  tz9.12lem1  9239  rankwflemb  9245  rankxpsuc  9334  scott0  9338  isnum2  9397  cardiun  9434  cardalephex  9540  dfac5lem4  9576  dfac12k  9597  cflim2  9713  cfss  9715  cfslb2n  9718  enfin2i  9771  fin23lem30  9792  itunitc  9871  axdc3lem2  9901  iundom2g  9990  pwcfsdom  10033  cfpwsdom  10034  tskr1om2  10218  genpelv  10450  prlem934  10483  suplem1pr  10502  supexpr  10504  supsrlem  10561  supsr  10562  fimaxre3  11614  iswrd  13905  caurcvgr  15068  caurcvg  15071  caucvg  15073  vdwapval  16354  restsspw  16753  mreunirn  16920  brssc  17133  arwhoma  17361  gexcl3  18769  dvdsr  19457  lspsnel  19833  lspprel  19924  ellspd  20557  iincld  21729  ssnei  21800  neindisj2  21813  neitr  21870  lecldbas  21909  tgcnp  21943  cncnp2  21971  lmmo  22070  is2ndc  22136  fbfinnfr  22531  fbunfip  22559  filunirn  22572  fbflim2  22667  flimcls  22675  hauspwpwf1  22677  flftg  22686  isfcls  22699  fclsbas  22711  isfcf  22724  ustfilxp  22903  ustbas  22918  restutop  22928  ucnima  22972  xmetunirn  23029  metss  23200  metrest  23216  restmetu  23262  qdensere  23461  elpi1  23736  lmmbr  23948  caun0  23971  nulmbl2  24226  itg2l  24419  aannenlem2  25014  taylfval  25043  ulmcl  25065  ulmpm  25067  ulmss  25081  tglnunirn  26431  ishpg  26642  edglnl  27025  uhgrwkspthlem1  27631  usgr2pth  27642  umgr2wlk  27824  elwwlks2ons3  27830  clwwlknun  27986  frgrncvvdeqlem3  28175  frgr2wwlkn0  28202  frgrreg  28268  hhcms  29075  hhsscms  29150  occllem  29175  occl  29176  chscllem2  29510  r19.29ffa  30333  rabfmpunirn  30504  rhmdvdsr  31033  kerunit  31038  tpr2rico  31373  gsumesum  31536  esumcst  31540  esumfsup  31547  esumpcvgval  31555  esumcvg  31563  sigaclcuni  31595  mbfmfun  31730  dya2icoseg2  31754  bnj66  32350  bnj517  32375  cusgr3cyclex  32604  rellysconn  32719  cvmliftlem15  32766  satffunlem2lem1  32872  poxp2  33335  poxp3  33341  orderseqlem  33345  nofun  33407  norn  33409  madeval2  33587  elmade  33597  dfrdg4  33792  brcolinear2  33899  brcolinear  33900  ellines  33993  poimirlem29  35356  volsupnfl  35372  unirep  35421  filbcmb  35448  islshpkrN  36686  ispointN  37308  pmapglbx  37335  rngunsnply  40480  elsetpreimafvbi  44266