Theorem rspcev 2758

Description: Restricted existential specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rspcev	|- ( ( A e. B /\ ps ) -> E. x e. B ph )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem rspcev

Step	Hyp	Ref	Expression
1		nfv 1489	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspce 2753	1 |- ( ( A e. B /\ ps ) -> E. x e. B ph )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1312   e. wcel 1461   E.wrex 2389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-rex 2394  df-v 2657

This theorem is referenced by:  rspceaimv  2765  rspc2ev  2772  rspc3ev  2774  rspceeqv  2775  reu6i  2842  rspesbca  2959  nn0suc  4476  elrnmpt1s  4747  elrnrexdm  5511  eldmrexrn  5513  foco2  5607  elabrex  5611  f1elima  5626  fcofo  5637  fliftfun  5649  fliftval  5653  f1oiso2  5680  fo1st  6007  fo2nd  6008  tfr0dm  6171  tfrlemisucaccv  6174  tfrlemi14d  6182  tfrexlem  6183  tfr1onlemsucaccv  6190  tfr1onlemres  6198  tfrcllemsucaccv  6203  tfrcllemres  6211  rdgss  6232  frecabcl  6248  nnaordex  6375  nnawordex  6376  ecelqsg  6434  snfig  6660  nnfi  6717  findcard  6733  fimax2gtrilemstep  6745  unsnfi  6758  eqsupti  6833  supmaxti  6841  supisoex  6846  infminti  6864  finomni  6960  isnumi  6985  oncardval  6989  archnqq  7167  prarloclemarch2  7169  prcdnql  7234  prcunqu  7235  prarloclemlo  7244  prarloclem5  7250  nqprm  7292  1idprl  7340  1idpru  7341  ltexpri  7363  prplnqu  7370  recexprlemm  7374  recexprlem1ssl  7383  recexprlem1ssu  7384  recexpr  7388  aptiprleml  7389  archpr  7393  cauappcvgprlemm  7395  cauappcvgprlemloc  7402  cauappcvgprlem1  7409  cauappcvgprlem2  7410  cauappcvgpr  7412  caucvgprlemm  7418  caucvgprlemloc  7425  caucvgprlem1  7429  caucvgprlem2  7430  caucvgpr  7432  caucvgprprlemmu  7445  caucvgprprlemopl  7447  caucvgprprlemopu  7449  caucvgprprlemloc  7453  caucvgprprlem1  7459  caucvgprprlem2  7460  caucvgprpr  7462  negexsr  7509  recexgt0sr  7510  caucvgsrlemgt1  7531  caucvgsrlemoffres  7536  axrnegex  7608  axprecex  7609  nntopi  7623  axcaucvglemres  7628  cnegex  7857  recexre  8252  recexap  8321  receuap  8337  sup3exmid  8619  cju  8623  nn2ge  8657  nominpos  8855  zdiv  9037  btwnz  9068  supinfneg  9286  infsupneg  9287  ublbneg  9301  lbzbi  9304  zq  9314  z2ge  9496  iccsupr  9636  exbtwnzlemstep  9912  exbtwnzlemex  9914  rebtwn2zlemstep  9917  rebtwn2z  9919  qbtwnre  9921  qbtwnxr  9922  expnbnd  10302  hashunlem  10437  shftlem  10475  shftfvalg  10477  shftfval  10480  caucvgre  10639  cvg1nlemres  10643  rexanuz  10646  rexuz3  10648  resqrexlemex  10683  caubnd2  10775  maxabslemval  10866  maxleast  10871  rexanre  10878  rexico  10879  fimaxre2  10884  minmax  10887  xrmaxiflemval  10905  xrmaxaddlem  10915  xrminmax  10920  climconst  10945  climshftlemg  10957  cn1lem  10969  serf0  11007  zsumdc  11039  fsum3  11042  fsum3cvg3  11051  mertenslemi1  11190  dvdsval2  11338  dvds0lem  11345  dvds1lem  11346  dvds2lem  11347  odd2np1lem  11411  odd2np1  11412  opeo  11436  omeo  11437  divalglemex  11461  zsupcllemstep  11480  infssuzex  11484  bezoutlemnewy  11524  bezoutlemaz  11531  bezoutlembz  11532  bezoutlemsup  11537  ncoprmgcdne1b  11610  exprmfct  11658  ennnfonelemex  11766  ennnfonelemhom  11767  ennnfonelemrn  11771  ennnfonelemnn0  11774  ennnfonelemim  11776  exmidunben  11778  ctinfomlemom  11779  ctinfom  11780  ctinf  11782  ctiunctlemf  11788  fiinbas  12053  topbas  12073  clsval  12117  neiint  12151  neipsm  12160  opnneissb  12161  opnssneib  12162  innei  12169  restbasg  12174  lmconst  12221  iscnp4  12223  cncnpi  12233  cnconst2  12238  cnptoprest  12244  cnpdis  12247  neitx  12273  txcnp  12276  blssps  12410  blss  12411  blssexps  12412  blssex  12413  ssblex  12414  blin2  12415  neibl  12474  metss2  12481  bdmopn  12487  metrest  12489  metcnp3  12494  tgioo  12526  tgqioo  12527  addcncntoplem  12531  bj-nn0suc0  12831  bj-inf2vnlem1  12851  nninfsellemeq  12891  nninfomnilem  12895  qdencn  12903