Theorem rexlimivw 3212

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3066

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 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3070  df-rex 3071

This theorem is referenced by:  r19.29vvaOLD  3268  r19.36v  3273  r19.44v  3282  r19.45v  3283  sbcreu  3810  eliun  4929  reusv3i  5328  elrnmptg  5871  fvelrnb  6839  fvelimab  6850  iinpreima  6955  fmpt  6993  fliftfun  7192  elrnmpo  7419  ovelrn  7457  onuninsuci  7696  fiunlem  7793  releldm2  7893  tfrlem4  8219  iiner  8587  elixpsn  8734  isfi  8773  card2on  9322  brttrcl  9480  tz9.12lem1  9554  rankwflemb  9560  rankxpsuc  9649  scott0  9653  isnum2  9712  cardiun  9749  cardalephex  9855  dfac5lem4  9891  dfac12k  9912  cflim2  10028  cfss  10030  cfslb2n  10033  enfin2i  10086  fin23lem30  10107  itunitc  10186  axdc3lem2  10216  iundom2g  10305  pwcfsdom  10348  cfpwsdom  10349  tskr1om2  10533  genpelv  10765  prlem934  10798  suplem1pr  10817  supexpr  10819  supsrlem  10876  supsr  10877  fimaxre3  11930  iswrd  14228  caurcvgr  15394  caurcvg  15397  caucvg  15399  vdwapval  16683  restsspw  17151  mreunirn  17319  brssc  17535  arwhoma  17769  gexcl3  19201  dvdsr  19897  lspsnel  20274  lspprel  20365  ellspd  21018  iincld  22199  ssnei  22270  neindisj2  22283  neitr  22340  lecldbas  22379  tgcnp  22413  cncnp2  22441  lmmo  22540  is2ndc  22606  fbfinnfr  23001  fbunfip  23029  filunirn  23042  fbflim2  23137  flimcls  23145  hauspwpwf1  23147  flftg  23156  isfcls  23169  fclsbas  23181  isfcf  23194  ustfilxp  23373  ustbas  23388  restutop  23398  ucnima  23442  xmetunirn  23499  metss  23673  metrest  23689  restmetu  23735  qdensere  23942  elpi1  24217  lmmbr  24431  caun0  24454  nulmbl2  24709  itg2l  24903  aannenlem2  25498  taylfval  25527  ulmcl  25549  ulmpm  25551  ulmss  25565  tglnunirn  26918  ishpg  27129  edglnl  27522  uhgrwkspthlem1  28130  usgr2pth  28141  umgr2wlk  28323  elwwlks2ons3  28329  clwwlknun  28485  frgrncvvdeqlem3  28674  frgr2wwlkn0  28701  frgrreg  28767  hhcms  29574  hhsscms  29649  occllem  29674  occl  29675  chscllem2  30009  r19.29ffa  30831  rabfmpunirn  30999  rhmdvdsr  31526  kerunit  31531  tpr2rico  31871  gsumesum  32036  esumcst  32040  esumfsup  32047  esumpcvgval  32055  esumcvg  32063  sigaclcuni  32095  mbfmfun  32230  dya2icoseg2  32254  bnj66  32849  bnj517  32874  cusgr3cyclex  33107  rellysconn  33222  cvmliftlem15  33269  satffunlem2lem1  33375  poxp2  33799  poxp3  33805  orderseqlem  33810  nofun  33861  norn  33863  madeval2  34046  elmade  34060  dfrdg4  34262  brcolinear2  34369  brcolinear  34370  ellines  34463  poimirlem29  35815  volsupnfl  35831  unirep  35880  filbcmb  35907  islshpkrN  37141  ispointN  37763  pmapglbx  37790  rngunsnply  41005  elsetpreimafvbi  44854