Theorem rexlimivw 3210

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  r19.29vvaOLD  3264  r19.36v  3269  r19.44v  3278  r19.45v  3279  sbcreu  3805  eliun  4925  reusv3i  5322  elrnmptg  5857  fvelrnb  6812  fvelimab  6823  iinpreima  6928  fmpt  6966  fliftfun  7163  elrnmpo  7388  ovelrn  7426  onuninsuci  7662  fiunlem  7758  releldm2  7857  tfrlem4  8181  iiner  8536  elixpsn  8683  isfi  8719  card2on  9243  tz9.12lem1  9476  rankwflemb  9482  rankxpsuc  9571  scott0  9575  isnum2  9634  cardiun  9671  cardalephex  9777  dfac5lem4  9813  dfac12k  9834  cflim2  9950  cfss  9952  cfslb2n  9955  enfin2i  10008  fin23lem30  10029  itunitc  10108  axdc3lem2  10138  iundom2g  10227  pwcfsdom  10270  cfpwsdom  10271  tskr1om2  10455  genpelv  10687  prlem934  10720  suplem1pr  10739  supexpr  10741  supsrlem  10798  supsr  10799  fimaxre3  11851  iswrd  14147  caurcvgr  15313  caurcvg  15316  caucvg  15318  vdwapval  16602  restsspw  17059  mreunirn  17227  brssc  17443  arwhoma  17676  gexcl3  19107  dvdsr  19803  lspsnel  20180  lspprel  20271  ellspd  20919  iincld  22098  ssnei  22169  neindisj2  22182  neitr  22239  lecldbas  22278  tgcnp  22312  cncnp2  22340  lmmo  22439  is2ndc  22505  fbfinnfr  22900  fbunfip  22928  filunirn  22941  fbflim2  23036  flimcls  23044  hauspwpwf1  23046  flftg  23055  isfcls  23068  fclsbas  23080  isfcf  23093  ustfilxp  23272  ustbas  23287  restutop  23297  ucnima  23341  xmetunirn  23398  metss  23570  metrest  23586  restmetu  23632  qdensere  23839  elpi1  24114  lmmbr  24327  caun0  24350  nulmbl2  24605  itg2l  24799  aannenlem2  25394  taylfval  25423  ulmcl  25445  ulmpm  25447  ulmss  25461  tglnunirn  26813  ishpg  27024  edglnl  27416  uhgrwkspthlem1  28022  usgr2pth  28033  umgr2wlk  28215  elwwlks2ons3  28221  clwwlknun  28377  frgrncvvdeqlem3  28566  frgr2wwlkn0  28593  frgrreg  28659  hhcms  29466  hhsscms  29541  occllem  29566  occl  29567  chscllem2  29901  r19.29ffa  30723  rabfmpunirn  30892  rhmdvdsr  31419  kerunit  31424  tpr2rico  31764  gsumesum  31927  esumcst  31931  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  sigaclcuni  31986  mbfmfun  32121  dya2icoseg2  32145  bnj66  32740  bnj517  32765  cusgr3cyclex  32998  rellysconn  33113  cvmliftlem15  33160  satffunlem2lem1  33266  brttrcl  33699  poxp2  33717  poxp3  33723  orderseqlem  33728  nofun  33779  norn  33781  madeval2  33964  elmade  33978  dfrdg4  34180  brcolinear2  34287  brcolinear  34288  ellines  34381  poimirlem29  35733  volsupnfl  35749  unirep  35798  filbcmb  35825  islshpkrN  37061  ispointN  37683  pmapglbx  37710  rngunsnply  40914  elsetpreimafvbi  44731