Theorem rspcev 2789

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1331   e. wcel 1480   E.wrex 2417

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688

This theorem is referenced by:  rspceaimv  2797  rspc2ev  2804  rspc3ev  2806  rspceeqv  2807  reu6i  2875  rspesbca  2993  brralrspcev  3986  nn0suc  4518  elrnmpt1s  4789  elrnrexdm  5559  eldmrexrn  5561  foco2  5655  elabrex  5659  f1elima  5674  fcofo  5685  fliftfun  5697  fliftval  5701  f1oiso2  5728  fo1st  6055  fo2nd  6056  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemsucaccv  6238  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllemres  6259  rdgss  6280  frecabcl  6296  nnaordex  6423  nnawordex  6424  ecelqsg  6482  snfig  6708  nnfi  6766  findcard  6782  fimax2gtrilemstep  6794  unsnfi  6807  eqsupti  6883  supmaxti  6891  supisoex  6896  infminti  6914  finomni  7012  isnumi  7038  oncardval  7042  archnqq  7225  prarloclemarch2  7227  prcdnql  7292  prcunqu  7293  prarloclemlo  7302  prarloclem5  7308  nqprm  7350  1idprl  7398  1idpru  7399  ltexpri  7421  prplnqu  7428  recexprlemm  7432  recexprlem1ssl  7441  recexprlem1ssu  7442  recexpr  7446  aptiprleml  7447  archpr  7451  cauappcvgprlemm  7453  cauappcvgprlemloc  7460  cauappcvgprlem1  7467  cauappcvgprlem2  7468  cauappcvgpr  7470  caucvgprlemm  7476  caucvgprlemloc  7483  caucvgprlem1  7487  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlem1  7517  caucvgprprlem2  7518  caucvgprpr  7520  suplocexprlemmu  7526  suplocexprlemloc  7529  suplocexpr  7533  negexsr  7580  recexgt0sr  7581  caucvgsrlemgt1  7603  caucvgsrlemoffres  7608  suplocsrlem  7616  axrnegex  7687  axprecex  7688  nntopi  7702  axcaucvglemres  7707  axpre-suploclemres  7709  cnegex  7940  recexre  8340  recexap  8414  receuap  8430  sup3exmid  8715  cju  8719  nn2ge  8753  nominpos  8957  zdiv  9139  btwnz  9170  supinfneg  9390  infsupneg  9391  ublbneg  9405  lbzbi  9408  zq  9418  z2ge  9609  iccsupr  9749  exbtwnzlemstep  10025  exbtwnzlemex  10027  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnre  10034  qbtwnxr  10035  expnbnd  10415  hashunlem  10550  shftlem  10588  shftfvalg  10590  shftfval  10593  caucvgre  10753  cvg1nlemres  10757  rexanuz  10760  rexuz3  10762  resqrexlemex  10797  caubnd2  10889  maxabslemval  10980  maxleast  10985  rexanre  10992  rexico  10993  fimaxre2  10998  minmax  11001  xrmaxiflemval  11019  xrmaxaddlem  11029  xrminmax  11034  climconst  11059  climshftlemg  11071  cn1lem  11083  serf0  11121  zsumdc  11153  fsum3  11156  fsum3cvg3  11165  mertenslemi1  11304  ntrivcvgap0  11318  dvdsval2  11496  dvds0lem  11503  dvds1lem  11504  dvds2lem  11505  odd2np1lem  11569  odd2np1  11570  opeo  11594  omeo  11595  divalglemex  11619  zsupcllemstep  11638  infssuzex  11642  bezoutlemnewy  11684  bezoutlemaz  11691  bezoutlembz  11692  bezoutlemsup  11697  ncoprmgcdne1b  11770  exprmfct  11818  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemrn  11932  ennnfonelemnn0  11935  ennnfonelemim  11937  exmidunben  11939  ctinfomlemom  11940  ctinfom  11941  ctinf  11943  ctiunctlemf  11951  fiinbas  12216  topbas  12236  clsval  12280  neiint  12314  neipsm  12323  opnneissb  12324  opnssneib  12325  innei  12332  restbasg  12337  lmconst  12385  iscnp4  12387  cncnpi  12397  cnconst2  12402  cnptoprest  12408  cnpdis  12411  neitx  12437  txcnp  12440  blssps  12596  blss  12597  blssexps  12598  blssex  12599  ssblex  12600  blin2  12601  neibl  12660  metss2  12667  bdmopn  12673  metrest  12675  metcnp3  12680  tgioo  12715  tgqioo  12716  addcncntoplem  12720  cnopnap  12763  dedekindeulemuub  12764  suplociccreex  12771  dedekindicclemuub  12773  ivthinclemlm  12781  ivthinclemum  12782  ivthinclemlopn  12783  ivthinclemuopn  12785  sin0pilem2  12863  bj-nn0suc0  13148  bj-inf2vnlem1  13168  nninfsellemeq  13210  nninfomnilem  13214  qdencn  13222