Theorem rexlimivw 3241

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  r19.29vva  3292  r19.36v  3296  r19.44v  3305  r19.45v  3306  sbcreu  3805  eliun  4885  reusv3i  5270  elrnmptg  5795  fvelrnb  6701  fvelimab  6712  iinpreima  6814  fmpt  6851  fliftfun  7044  elrnmpo  7266  ovelrn  7304  onuninsuci  7535  fiunlem  7625  releldm2  7724  tfrlem4  7998  iiner  8352  elixpsn  8484  isfi  8516  card2on  9002  tz9.12lem1  9200  rankwflemb  9206  rankxpsuc  9295  scott0  9299  isnum2  9358  cardiun  9395  cardalephex  9501  dfac5lem4  9537  dfac12k  9558  cflim2  9674  cfss  9676  cfslb2n  9679  enfin2i  9732  fin23lem30  9753  itunitc  9832  axdc3lem2  9862  iundom2g  9951  pwcfsdom  9994  cfpwsdom  9995  tskr1om2  10179  genpelv  10411  prlem934  10444  suplem1pr  10463  supexpr  10465  supsrlem  10522  supsr  10523  fimaxre3  11575  iswrd  13859  caurcvgr  15022  caurcvg  15025  caucvg  15027  vdwapval  16299  restsspw  16697  mreunirn  16864  brssc  17076  arwhoma  17297  gexcl3  18704  dvdsr  19392  lspsnel  19768  lspprel  19859  ellspd  20491  iincld  21644  ssnei  21715  neindisj2  21728  neitr  21785  lecldbas  21824  tgcnp  21858  cncnp2  21886  lmmo  21985  is2ndc  22051  fbfinnfr  22446  fbunfip  22474  filunirn  22487  fbflim2  22582  flimcls  22590  hauspwpwf1  22592  flftg  22601  isfcls  22614  fclsbas  22626  isfcf  22639  ustfilxp  22818  ustbas  22833  restutop  22843  ucnima  22887  xmetunirn  22944  metss  23115  metrest  23131  restmetu  23177  qdensere  23375  elpi1  23650  lmmbr  23862  caun0  23885  nulmbl2  24140  itg2l  24333  aannenlem2  24925  taylfval  24954  ulmcl  24976  ulmpm  24978  ulmss  24992  tglnunirn  26342  ishpg  26553  edglnl  26936  uhgrwkspthlem1  27542  usgr2pth  27553  umgr2wlk  27735  elwwlks2ons3  27741  clwwlknun  27897  frgrncvvdeqlem3  28086  frgr2wwlkn0  28113  frgrreg  28179  hhcms  28986  hhsscms  29061  occllem  29086  occl  29087  chscllem2  29421  r19.29ffa  30244  rabfmpunirn  30416  rhmdvdsr  30942  kerunit  30947  tpr2rico  31265  gsumesum  31428  esumcst  31432  esumfsup  31439  esumpcvgval  31447  esumcvg  31455  sigaclcuni  31487  mbfmfun  31622  dya2icoseg2  31646  bnj66  32242  bnj517  32267  cusgr3cyclex  32496  rellysconn  32611  cvmliftlem15  32658  satffunlem2lem1  32764  orderseqlem  33207  nofun  33269  norn  33271  madeval2  33403  dfrdg4  33525  brcolinear2  33632  brcolinear  33633  ellines  33726  poimirlem29  35086  volsupnfl  35102  unirep  35151  filbcmb  35178  islshpkrN  36416  ispointN  37038  pmapglbx  37065  rngunsnply  40117  elsetpreimafvbi  43908