Theorem rspcev 2834

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 1521	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspce 2829	1 |- ( ( A e. B /\ ps ) -> E. x e. B ph )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   E.wrex 2449

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732

This theorem is referenced by:  rspceaimv  2842  rspc2ev  2849  rspc3ev  2851  rspceeqv  2852  reu6i  2921  rspesbca  3039  brralrspcev  4047  nn0suc  4588  elrnmpt1s  4861  elrnrexdm  5635  eldmrexrn  5637  foco2  5733  elabrex  5737  f1elima  5752  fcofo  5763  fliftfun  5775  fliftval  5779  f1oiso2  5806  fo1st  6136  fo2nd  6137  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemsucaccv  6320  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllemres  6341  rdgss  6362  frecabcl  6378  nnaordex  6507  nnawordex  6508  ecelqsg  6566  snfig  6792  nnfi  6850  findcard  6866  fimax2gtrilemstep  6878  unsnfi  6896  eqsupti  6973  supmaxti  6981  supisoex  6986  infminti  7004  finomni  7116  nninfwlpoimlemginf  7152  isnumi  7159  oncardval  7163  archnqq  7379  prarloclemarch2  7381  prcdnql  7446  prcunqu  7447  prarloclemlo  7456  prarloclem5  7462  nqprm  7504  1idprl  7552  1idpru  7553  ltexpri  7575  prplnqu  7582  recexprlemm  7586  recexprlem1ssl  7595  recexprlem1ssu  7596  recexpr  7600  aptiprleml  7601  archpr  7605  cauappcvgprlemm  7607  cauappcvgprlemloc  7614  cauappcvgprlem1  7621  cauappcvgprlem2  7622  cauappcvgpr  7624  caucvgprlemm  7630  caucvgprlemloc  7637  caucvgprlem1  7641  caucvgprlem2  7642  caucvgpr  7644  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgprpr  7674  suplocexprlemmu  7680  suplocexprlemloc  7683  suplocexpr  7687  negexsr  7734  recexgt0sr  7735  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  suplocsrlem  7770  axrnegex  7841  axprecex  7842  nntopi  7856  axcaucvglemres  7861  axpre-suploclemres  7863  cnegex  8097  recexre  8497  recexap  8571  receuap  8587  sup3exmid  8873  cju  8877  nn2ge  8911  nominpos  9115  zdiv  9300  btwnz  9331  supinfneg  9554  infsupneg  9555  ublbneg  9572  lbzbi  9575  zq  9585  z2ge  9783  iccsupr  9923  exbtwnzlemstep  10204  exbtwnzlemex  10206  rebtwn2zlemstep  10209  rebtwn2z  10211  qbtwnre  10213  qbtwnxr  10214  expnbnd  10599  hashunlem  10739  shftlem  10780  shftfvalg  10782  shftfval  10785  caucvgre  10945  cvg1nlemres  10949  rexanuz  10952  rexuz3  10954  resqrexlemex  10989  caubnd2  11081  maxabslemval  11172  maxleast  11177  rexanre  11184  rexico  11185  fimaxre2  11190  minmax  11193  xrmaxiflemval  11213  xrmaxaddlem  11223  xrminmax  11228  climconst  11253  climshftlemg  11265  cn1lem  11277  serf0  11315  zsumdc  11347  fsum3  11350  fsum3cvg3  11359  mertenslemi1  11498  ntrivcvgap0  11512  zproddc  11542  fprodseq  11546  fprodntrivap  11547  dvdsval2  11752  dvds0lem  11763  dvds1lem  11764  dvds2lem  11765  odd2np1lem  11831  odd2np1  11832  opeo  11856  omeo  11857  divalglemex  11881  zsupcllemstep  11900  infssuzex  11904  suprzubdc  11907  zsupssdc  11909  bezoutlemnewy  11951  bezoutlemaz  11958  bezoutlembz  11959  bezoutlemsup  11964  nnwodc  11991  uzwodc  11992  ncoprmgcdne1b  12043  exprmfct  12092  reumodprminv  12207  modprm0  12208  nnnn0modprm0  12209  pythagtriplem19  12236  pcprmpw2  12286  pockthi  12310  infpnlem2  12312  ennnfonelemex  12369  ennnfonelemhom  12370  ennnfonelemrn  12374  ennnfonelemnn0  12377  ennnfonelemim  12379  exmidunben  12381  ctinfomlemom  12382  ctinfom  12383  ctinf  12385  ctiunctlemf  12393  ismgmid2  12634  mgmidsssn0  12638  ismndd  12673  isgrpd2  12727  isgrpd  12729  fiinbas  12841  topbas  12861  clsval  12905  neiint  12939  neipsm  12948  opnneissb  12949  opnssneib  12950  innei  12957  restbasg  12962  lmconst  13010  iscnp4  13012  cncnpi  13022  cnconst2  13027  cnptoprest  13033  cnpdis  13036  neitx  13062  txcnp  13065  blssps  13221  blss  13222  blssexps  13223  blssex  13224  ssblex  13225  blin2  13226  neibl  13285  metss2  13292  bdmopn  13298  metrest  13300  metcnp3  13305  tgioo  13340  tgqioo  13341  addcncntoplem  13345  cnopnap  13388  dedekindeulemuub  13389  suplociccreex  13396  dedekindicclemuub  13398  ivthinclemlm  13406  ivthinclemum  13407  ivthinclemlopn  13408  ivthinclemuopn  13410  reeff1oleme  13487  sin0pilem2  13497  bj-nn0suc0  13985  bj-inf2vnlem1  14005  nninfsellemeq  14047  nninfomnilem  14051  qdencn  14059  trirec0  14076