Theorem rexlimivw 3029

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  r19.29vva  3081  r19.36v  3085  r19.44v  3094  r19.45v  3095  sbcreu  3515  eliun  4524  reusv3i  4875  elrnmptg  5375  fvelrnb  6243  fvelimab  6253  iinpreima  6345  fmpt  6381  fliftfun  6562  elrnmpt2  6773  ovelrn  6810  onuninsuci  7040  fun11iun  7126  releldm2  7218  tfrlem4  7475  iiner  7819  elixpsn  7947  isfi  7979  card2on  8459  tz9.12lem1  8650  rankwflemb  8656  rankxpsuc  8745  scott0  8749  isnum2  8771  cardiun  8808  cardalephex  8913  dfac5lem4  8949  dfac12k  8969  cflim2  9085  cfss  9087  cfslb2n  9090  enfin2i  9143  fin23lem30  9164  itunitc  9243  axdc3lem2  9273  iundom2g  9362  pwcfsdom  9405  cfpwsdom  9406  tskr1om2  9590  genpelv  9822  prlem934  9855  suplem1pr  9874  supexpr  9876  supsrlem  9932  supsr  9933  fimaxre3  10970  iswrd  13307  caurcvgr  14404  caurcvg  14407  caucvg  14409  vdwapval  15677  restsspw  16092  mreunirn  16261  brssc  16474  arwhoma  16695  gexcl3  18002  dvdsr  18646  lspsnel  19003  lspprel  19094  ellspd  20141  iincld  20843  ssnei  20914  neindisj2  20927  neitr  20984  lecldbas  21023  tgcnp  21057  cncnp2  21085  lmmo  21184  is2ndc  21249  fbfinnfr  21645  fbunfip  21673  filunirn  21686  fbflim2  21781  flimcls  21789  hauspwpwf1  21791  flftg  21800  isfcls  21813  fclsbas  21825  isfcf  21838  ustfilxp  22016  ustbas  22031  restutop  22041  ucnima  22085  xmetunirn  22142  metss  22313  metrest  22329  restmetu  22375  qdensere  22573  elpi1  22845  lmmbr  23056  caun0  23079  nulmbl2  23304  itg2l  23496  aannenlem2  24084  taylfval  24113  ulmcl  24135  ulmpm  24137  ulmss  24151  tglnunirn  25443  ishpg  25651  edglnl  26038  uhgrwkspthlem1  26649  usgr2pth  26660  umgr2wlk  26845  frgrncvvdeqlem3  27165  frgr2wwlkn0  27192  frgrreg  27252  hhcms  28060  hhsscms  28136  occllem  28162  occl  28163  chscllem2  28497  r19.29ffa  29320  rabfmpunirn  29453  rhmdvdsr  29818  kerunit  29823  tpr2rico  29958  gsumesum  30121  esumcst  30125  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  sigaclcuni  30181  mbfmfun  30316  dya2icoseg2  30340  bnj66  30930  bnj517  30955  rellysconn  31233  cvmliftlem15  31280  orderseqlem  31749  nofun  31802  norn  31804  madeval2  31936  dfrdg4  32058  brcolinear2  32165  brcolinear  32166  ellines  32259  poimirlem29  33438  volsupnfl  33454  unirep  33507  filbcmb  33535  islshpkrN  34407  ispointN  35028  pmapglbx  35055  rngunsnply  37743