Theorem rexlimivw 3282

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  r19.29vva  3336  r19.29vvaOLD  3337  r19.36v  3342  r19.44v  3352  r19.45v  3353  sbcreu  3858  eliun  4915  reusv3i  5296  elrnmptg  5825  fvelrnb  6720  fvelimab  6731  iinpreima  6831  fmpt  6868  fliftfun  7059  elrnmpo  7281  ovelrn  7318  onuninsuci  7549  fiunlem  7637  releldm2  7736  tfrlem4  8009  iiner  8363  elixpsn  8495  isfi  8527  card2on  9012  tz9.12lem1  9210  rankwflemb  9216  rankxpsuc  9305  scott0  9309  isnum2  9368  cardiun  9405  cardalephex  9510  dfac5lem4  9546  dfac12k  9567  cflim2  9679  cfss  9681  cfslb2n  9684  enfin2i  9737  fin23lem30  9758  itunitc  9837  axdc3lem2  9867  iundom2g  9956  pwcfsdom  9999  cfpwsdom  10000  tskr1om2  10184  genpelv  10416  prlem934  10449  suplem1pr  10468  supexpr  10470  supsrlem  10527  supsr  10528  fimaxre3  11581  iswrd  13857  caurcvgr  15024  caurcvg  15027  caucvg  15029  vdwapval  16303  restsspw  16699  mreunirn  16866  brssc  17078  arwhoma  17299  gexcl3  18706  dvdsr  19390  lspsnel  19769  lspprel  19860  ellspd  20940  iincld  21641  ssnei  21712  neindisj2  21725  neitr  21782  lecldbas  21821  tgcnp  21855  cncnp2  21883  lmmo  21982  is2ndc  22048  fbfinnfr  22443  fbunfip  22471  filunirn  22484  fbflim2  22579  flimcls  22587  hauspwpwf1  22589  flftg  22598  isfcls  22611  fclsbas  22623  isfcf  22636  ustfilxp  22815  ustbas  22830  restutop  22840  ucnima  22884  xmetunirn  22941  metss  23112  metrest  23128  restmetu  23174  qdensere  23372  elpi1  23643  lmmbr  23855  caun0  23878  nulmbl2  24131  itg2l  24324  aannenlem2  24912  taylfval  24941  ulmcl  24963  ulmpm  24965  ulmss  24979  tglnunirn  26328  ishpg  26539  edglnl  26922  uhgrwkspthlem1  27528  usgr2pth  27539  umgr2wlk  27722  elwwlks2ons3  27728  clwwlknun  27885  frgrncvvdeqlem3  28074  frgr2wwlkn0  28101  frgrreg  28167  hhcms  28974  hhsscms  29049  occllem  29074  occl  29075  chscllem2  29409  r19.29ffa  30231  rabfmpunirn  30392  rhmdvdsr  30886  kerunit  30891  tpr2rico  31150  gsumesum  31313  esumcst  31317  esumfsup  31324  esumpcvgval  31332  esumcvg  31340  sigaclcuni  31372  mbfmfun  31507  dya2icoseg2  31531  bnj66  32127  bnj517  32152  cusgr3cyclex  32378  rellysconn  32493  cvmliftlem15  32540  satffunlem2lem1  32646  orderseqlem  33089  nofun  33151  norn  33153  madeval2  33285  dfrdg4  33407  brcolinear2  33514  brcolinear  33515  ellines  33608  poimirlem29  34915  volsupnfl  34931  unirep  34982  filbcmb  35009  islshpkrN  36250  ispointN  36872  pmapglbx  36899  rngunsnply  39766  elsetpreimafvbi  43545