Theorem rspcev 2911

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805

This theorem is referenced by:  rspceaimv  2919  rspc2ev  2926  rspc3ev  2928  rspceeqv  2929  reu6i  2998  rspesbca  3118  brralrspcev  4152  nn0suc  4708  elrnmpt1s  4988  elrnrexdm  5794  eldmrexrn  5796  foco2  5904  elabrex  5908  elabrexg  5909  f1elima  5924  fcofo  5935  fliftfun  5947  fliftval  5951  f1oiso2  5978  fo1st  6329  fo2nd  6330  tfr0dm  6531  tfrlemisucaccv  6534  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemsucaccv  6550  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllemres  6571  rdgss  6592  frecabcl  6608  nnaordex  6739  nnawordex  6740  ecelqsg  6800  snfig  7032  nnfi  7102  findcard  7120  fimax2gtrilemstep  7133  unsnfi  7154  eqsupti  7255  supmaxti  7263  supisoex  7268  infminti  7286  finomni  7399  nninfwlpoimlemginf  7435  isnumi  7446  oncardval  7450  archnqq  7697  prarloclemarch2  7699  prcdnql  7764  prcunqu  7765  prarloclemlo  7774  prarloclem5  7780  nqprm  7822  1idprl  7870  1idpru  7871  ltexpri  7893  prplnqu  7900  recexprlemm  7904  recexprlem1ssl  7913  recexprlem1ssu  7914  recexpr  7918  aptiprleml  7919  archpr  7923  cauappcvgprlemm  7925  cauappcvgprlemloc  7932  cauappcvgprlem1  7939  cauappcvgprlem2  7940  cauappcvgpr  7942  caucvgprlemm  7948  caucvgprlemloc  7955  caucvgprlem1  7959  caucvgprlem2  7960  caucvgpr  7962  caucvgprprlemmu  7975  caucvgprprlemopl  7977  caucvgprprlemopu  7979  caucvgprprlemloc  7983  caucvgprprlem1  7989  caucvgprprlem2  7990  caucvgprpr  7992  suplocexprlemmu  7998  suplocexprlemloc  8001  suplocexpr  8005  negexsr  8052  recexgt0sr  8053  caucvgsrlemgt1  8075  caucvgsrlemoffres  8080  suplocsrlem  8088  axrnegex  8159  axprecex  8160  nntopi  8174  axcaucvglemres  8179  axpre-suploclemres  8181  cnegex  8416  recexre  8817  recexap  8892  receuap  8908  rerecapb  9082  sup3exmid  9196  cju  9200  nn2ge  9235  nominpos  9441  zdiv  9629  btwnz  9660  supinfneg  9890  infsupneg  9891  ublbneg  9908  lbzbi  9911  zq  9921  z2ge  10122  iccsupr  10262  zsupcllemstep  10552  infssuzex  10556  suprzubdc  10559  zsupssdc  10561  exbtwnzlemstep  10570  exbtwnzlemex  10572  rebtwn2zlemstep  10575  rebtwn2z  10577  qbtwnre  10579  qbtwnxr  10580  expnbnd  10988  hashunlem  11130  iswrdinn0  11184  shftlem  11456  shftfvalg  11458  shftfval  11461  caucvgre  11621  cvg1nlemres  11625  rexanuz  11628  rexuz3  11630  resqrexlemex  11665  caubnd2  11757  maxabslemval  11848  maxleast  11853  rexanre  11860  rexico  11861  fimaxre2  11867  minmax  11870  xrmaxiflemval  11890  xrmaxaddlem  11900  xrminmax  11905  climconst  11930  climshftlemg  11942  cn1lem  11954  serf0  11992  zsumdc  12025  fsum3  12028  fsum3cvg3  12037  mertenslemi1  12176  ntrivcvgap0  12190  zproddc  12220  fprodseq  12224  fprodntrivap  12225  dvdsval2  12431  dvds0lem  12442  dvds1lem  12443  dvds2lem  12444  odd2np1lem  12513  odd2np1  12514  opeo  12538  omeo  12539  divalglemex  12563  bezoutlemnewy  12647  bezoutlemaz  12654  bezoutlembz  12655  bezoutlemsup  12660  nnwodc  12687  uzwodc  12688  ncoprmgcdne1b  12741  exprmfct  12790  reumodprminv  12906  modprm0  12907  nnnn0modprm0  12908  pythagtriplem19  12935  pcprmpw2  12986  pockthi  13011  infpnlem2  13013  ennnfonelemex  13115  ennnfonelemhom  13116  ennnfonelemrn  13120  ennnfonelemnn0  13123  ennnfonelemim  13125  exmidunben  13127  ctinfomlemom  13128  ctinfom  13129  ctinf  13131  ctiunctlemf  13139  ismgmid2  13543  mgmidsssn0  13547  ismndd  13600  isgrpd2  13684  isgrpd  13686  imasgrp2  13777  mhmmnd  13783  ghmgrp  13785  dvdsrmuld  14191  dvdsr01  14199  rhmdvdsr  14270  lspf  14485  lspval  14486  lssats2  14510  fiinbas  14860  topbas  14878  clsval  14922  neiint  14956  neipsm  14965  opnneissb  14966  opnssneib  14967  innei  14974  restbasg  14979  lmconst  15027  iscnp4  15029  cncnpi  15039  cnconst2  15044  cnptoprest  15050  cnpdis  15053  neitx  15079  txcnp  15082  blssps  15238  blss  15239  blssexps  15240  blssex  15241  ssblex  15242  blin2  15243  neibl  15302  metss2  15309  bdmopn  15315  metrest  15317  metcnp3  15322  tgioo  15365  tgqioo  15366  addcncntoplem  15372  cnopnap  15422  dedekindeulemuub  15428  suplociccreex  15435  dedekindicclemuub  15437  ivthinclemlm  15445  ivthinclemum  15446  ivthinclemlopn  15447  ivthinclemuopn  15449  ivthreinc  15456  elply2  15546  reeff1oleme  15583  sin0pilem2  15593  sgmnncl  15802  dvdsppwf1o  15803  perfect  15815  bj-nn0suc0  16666  bj-inf2vnlem1  16686  3dom  16708  nninfsellemeq  16740  nninfomnilem  16744  qdencn  16755  trirec0  16776  qdiff  16781