Theorem rspcev 2923

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   e. wcel 2205   E.wrex 2523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817

This theorem is referenced by:  rspcedvdw  2930  rspceaimv  2932  rspc2ev  2939  rspc3ev  2941  rspceeqv  2942  reu6i  3011  rspesbca  3131  brralrspcev  4173  nn0suc  4731  elrnmpt1s  5012  elrnrexdm  5821  eldmrexrn  5823  foco2  5932  elabrex  5936  elabrexg  5937  f1elima  5952  fcofo  5963  fliftfun  5975  fliftval  5979  f1oiso2  6006  fo1st  6364  fo2nd  6365  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemsucaccv  6585  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllemres  6606  rdgss  6627  frecabcl  6643  nnaordex  6774  nnawordex  6775  ecelqsg  6835  snfig  7069  nnfi  7140  findcard  7158  fimax2gtrilemstep  7171  unsnfi  7192  eqsupti  7300  supmaxti  7308  supisoex  7313  infminti  7331  finomni  7444  nninfwlpoimlemginf  7480  isnumi  7491  oncardval  7495  archnqq  7748  prarloclemarch2  7750  prcdnql  7815  prcunqu  7816  prarloclemlo  7825  prarloclem5  7831  nqprm  7873  1idprl  7921  1idpru  7922  ltexpri  7944  prplnqu  7951  recexprlemm  7955  recexprlem1ssl  7964  recexprlem1ssu  7965  recexpr  7969  aptiprleml  7970  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemloc  7983  cauappcvgprlem1  7990  cauappcvgprlem2  7991  cauappcvgpr  7993  caucvgprlemm  7999  caucvgprlemloc  8006  caucvgprlem1  8010  caucvgprlem2  8011  caucvgpr  8013  caucvgprprlemmu  8026  caucvgprprlemopl  8028  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlem1  8040  caucvgprprlem2  8041  caucvgprpr  8043  suplocexprlemmu  8049  suplocexprlemloc  8052  suplocexpr  8056  negexsr  8103  recexgt0sr  8104  caucvgsrlemgt1  8126  caucvgsrlemoffres  8131  suplocsrlem  8139  axrnegex  8210  axprecex  8211  nntopi  8225  axcaucvglemres  8230  axpre-suploclemres  8232  cnegex  8467  recexre  8869  recexap  8944  receuap  8960  rerecapb  9134  sup3exmid  9248  cju  9252  nn2ge  9287  nominpos  9493  zdiv  9684  btwnz  9715  supinfneg  9945  infsupneg  9946  ublbneg  9963  lbzbi  9966  zq  9976  z2ge  10178  iccsupr  10318  zsupcllemstep  10611  infssuzex  10615  suprzubdc  10620  zsupssdc  10622  exbtwnzlemstep  10631  exbtwnzlemex  10633  rebtwn2zlemstep  10636  rebtwn2z  10638  qbtwnre  10640  qbtwnxr  10641  expnbnd  11050  hashunlem  11193  iswrdinn0  11254  shftlem  11526  shftfvalg  11528  shftfval  11531  caucvgre  11691  cvg1nlemres  11695  rexanuz  11698  rexuz3  11700  resqrexlemex  11735  caubnd2  11827  maxabslemval  11918  maxleast  11923  rexanre  11930  rexico  11931  fimaxre2  11937  minmax  11940  xrmaxiflemval  11960  xrmaxaddlem  11970  xrminmax  11975  climconst  12000  climshftlemg  12012  cn1lem  12024  serf0  12062  zsumdc  12095  fsum3  12098  fsum3cvg3  12107  mertenslemi1  12246  ntrivcvgap0  12260  zproddc  12290  fprodseq  12294  fprodntrivap  12295  dvdsval2  12501  dvds0lem  12512  dvds1lem  12513  dvds2lem  12514  odd2np1lem  12583  odd2np1  12584  opeo  12608  omeo  12609  divalglemex  12633  bezoutlemnewy  12717  bezoutlemaz  12724  bezoutlembz  12725  bezoutlemsup  12730  nnwodc  12757  uzwodc  12758  ncoprmgcdne1b  12811  exprmfct  12860  reumodprminv  12976  modprm0  12977  nnnn0modprm0  12978  pythagtriplem19  13005  pcprmpw2  13056  pockthi  13081  infpnlem2  13083  ballotfilem4  13185  ballotfilemic  13194  ennnfonelemex  13249  ennnfonelemhom  13250  ennnfonelemrn  13254  ennnfonelemnn0  13257  ennnfonelemim  13259  exmidunben  13261  ctinfomlemom  13262  ctinfom  13263  ctinf  13265  ctiunctlemf  13273  ismgmid2  13643  mgmidsssn0  13647  ismndd  13698  isgrpd2  13776  isgrpd  13778  imasgrp2  13863  mhmmnd  13869  ghmgrp  13871  dvdsrmuld  14341  dvdsr01  14349  rhmdvdsr  14420  lspf  14663  lspval  14664  lssats2  14688  fiinbas  15040  topbas  15058  clsval  15102  neiint  15136  neipsm  15145  opnneissb  15146  opnssneib  15147  innei  15154  restbasg  15159  lmconst  15207  iscnp4  15209  cncnpi  15219  cnconst2  15224  cnptoprest  15230  cnpdis  15233  neitx  15259  txcnp  15262  blssps  15418  blss  15419  blssexps  15420  blssex  15421  ssblex  15422  blin2  15423  neibl  15482  metss2  15489  bdmopn  15495  metrest  15497  metcnp3  15502  tgioo  15545  tgqioo  15546  addcncntoplem  15552  cnopnap  15602  dedekindeulemuub  15608  suplociccreex  15615  dedekindicclemuub  15617  ivthinclemlm  15625  ivthinclemum  15626  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthreinc  15636  elply2  15726  reeff1oleme  15763  sin0pilem2  15773  sgmnncl  15982  dvdsppwf1o  15983  perfect  15995  bj-nn0suc0  16846  bj-inf2vnlem1  16866  3dom  16888  nninfsellemeq  16918  nninfomnilem  16922  qdencn  16933  trirec0  16954  qdiff  16959