Theorem rspcev 2921

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 2916	1 |- ( ( A e. B /\ ps ) -> E. x e. B ph )

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

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815

This theorem is referenced by:  rspceaimv  2929  rspc2ev  2936  rspc3ev  2938  rspceeqv  2939  reu6i  3008  rspesbca  3128  brralrspcev  4168  nn0suc  4726  elrnmpt1s  5007  elrnrexdm  5816  eldmrexrn  5818  foco2  5926  elabrex  5930  elabrexg  5931  f1elima  5946  fcofo  5957  fliftfun  5969  fliftval  5973  f1oiso2  6000  fo1st  6351  fo2nd  6352  tfr0dm  6553  tfrlemisucaccv  6556  tfrlemi14d  6564  tfrexlem  6565  tfr1onlemsucaccv  6572  tfr1onlemres  6580  tfrcllemsucaccv  6585  tfrcllemres  6593  rdgss  6614  frecabcl  6630  nnaordex  6761  nnawordex  6762  ecelqsg  6822  snfig  7056  nnfi  7127  findcard  7145  fimax2gtrilemstep  7158  unsnfi  7179  eqsupti  7287  supmaxti  7295  supisoex  7300  infminti  7318  finomni  7431  nninfwlpoimlemginf  7467  isnumi  7478  oncardval  7482  archnqq  7732  prarloclemarch2  7734  prcdnql  7799  prcunqu  7800  prarloclemlo  7809  prarloclem5  7815  nqprm  7857  1idprl  7905  1idpru  7906  ltexpri  7928  prplnqu  7935  recexprlemm  7939  recexprlem1ssl  7948  recexprlem1ssu  7949  recexpr  7953  aptiprleml  7954  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemloc  7967  cauappcvgprlem1  7974  cauappcvgprlem2  7975  cauappcvgpr  7977  caucvgprlemm  7983  caucvgprlemloc  7990  caucvgprlem1  7994  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgprpr  8027  suplocexprlemmu  8033  suplocexprlemloc  8036  suplocexpr  8040  negexsr  8087  recexgt0sr  8088  caucvgsrlemgt1  8110  caucvgsrlemoffres  8115  suplocsrlem  8123  axrnegex  8194  axprecex  8195  nntopi  8209  axcaucvglemres  8214  axpre-suploclemres  8216  cnegex  8451  recexre  8852  recexap  8927  receuap  8943  rerecapb  9117  sup3exmid  9231  cju  9235  nn2ge  9270  nominpos  9476  zdiv  9666  btwnz  9697  supinfneg  9927  infsupneg  9928  ublbneg  9945  lbzbi  9948  zq  9958  z2ge  10159  iccsupr  10299  zsupcllemstep  10589  infssuzex  10593  suprzubdc  10596  zsupssdc  10598  exbtwnzlemstep  10607  exbtwnzlemex  10609  rebtwn2zlemstep  10612  rebtwn2z  10614  qbtwnre  10616  qbtwnxr  10617  expnbnd  11025  hashunlem  11168  iswrdinn0  11229  shftlem  11501  shftfvalg  11503  shftfval  11506  caucvgre  11666  cvg1nlemres  11670  rexanuz  11673  rexuz3  11675  resqrexlemex  11710  caubnd2  11802  maxabslemval  11893  maxleast  11898  rexanre  11905  rexico  11906  fimaxre2  11912  minmax  11915  xrmaxiflemval  11935  xrmaxaddlem  11945  xrminmax  11950  climconst  11975  climshftlemg  11987  cn1lem  11999  serf0  12037  zsumdc  12070  fsum3  12073  fsum3cvg3  12082  mertenslemi1  12221  ntrivcvgap0  12235  zproddc  12265  fprodseq  12269  fprodntrivap  12270  dvdsval2  12476  dvds0lem  12487  dvds1lem  12488  dvds2lem  12489  odd2np1lem  12558  odd2np1  12559  opeo  12583  omeo  12584  divalglemex  12608  bezoutlemnewy  12692  bezoutlemaz  12699  bezoutlembz  12700  bezoutlemsup  12705  nnwodc  12732  uzwodc  12733  ncoprmgcdne1b  12786  exprmfct  12835  reumodprminv  12951  modprm0  12952  nnnn0modprm0  12953  pythagtriplem19  12980  pcprmpw2  13031  pockthi  13056  infpnlem2  13058  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemrn  13170  ennnfonelemnn0  13173  ennnfonelemim  13175  exmidunben  13177  ctinfomlemom  13178  ctinfom  13179  ctinf  13181  ctiunctlemf  13189  ismgmid2  13593  mgmidsssn0  13597  ismndd  13650  isgrpd2  13734  isgrpd  13736  imasgrp2  13827  mhmmnd  13833  ghmgrp  13835  dvdsrmuld  14241  dvdsr01  14249  rhmdvdsr  14320  lspf  14537  lspval  14538  lssats2  14562  fiinbas  14914  topbas  14932  clsval  14976  neiint  15010  neipsm  15019  opnneissb  15020  opnssneib  15021  innei  15028  restbasg  15033  lmconst  15081  iscnp4  15083  cncnpi  15093  cnconst2  15098  cnptoprest  15104  cnpdis  15107  neitx  15133  txcnp  15136  blssps  15292  blss  15293  blssexps  15294  blssex  15295  ssblex  15296  blin2  15297  neibl  15356  metss2  15363  bdmopn  15369  metrest  15371  metcnp3  15376  tgioo  15419  tgqioo  15420  addcncntoplem  15426  cnopnap  15476  dedekindeulemuub  15482  suplociccreex  15489  dedekindicclemuub  15491  ivthinclemlm  15499  ivthinclemum  15500  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthreinc  15510  elply2  15600  reeff1oleme  15637  sin0pilem2  15647  sgmnncl  15856  dvdsppwf1o  15857  perfect  15869  bj-nn0suc0  16720  bj-inf2vnlem1  16740  3dom  16762  nninfsellemeq  16792  nninfomnilem  16796  qdencn  16807  trirec0  16828  qdiff  16833