Theorem rspcev 2877

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2176   E.wrex 2485

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774

This theorem is referenced by:  rspceaimv  2885  rspc2ev  2892  rspc3ev  2894  rspceeqv  2895  reu6i  2964  rspesbca  3083  brralrspcev  4103  nn0suc  4653  elrnmpt1s  4929  elrnrexdm  5721  eldmrexrn  5723  foco2  5824  elabrex  5828  elabrexg  5829  f1elima  5844  fcofo  5855  fliftfun  5867  fliftval  5871  f1oiso2  5898  fo1st  6245  fo2nd  6246  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemi14d  6421  tfrexlem  6422  tfr1onlemsucaccv  6429  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllemres  6450  rdgss  6471  frecabcl  6487  nnaordex  6616  nnawordex  6617  ecelqsg  6677  snfig  6908  nnfi  6971  findcard  6987  fimax2gtrilemstep  6999  unsnfi  7018  eqsupti  7100  supmaxti  7108  supisoex  7113  infminti  7131  finomni  7244  nninfwlpoimlemginf  7280  isnumi  7291  oncardval  7295  archnqq  7532  prarloclemarch2  7534  prcdnql  7599  prcunqu  7600  prarloclemlo  7609  prarloclem5  7615  nqprm  7657  1idprl  7705  1idpru  7706  ltexpri  7728  prplnqu  7735  recexprlemm  7739  recexprlem1ssl  7748  recexprlem1ssu  7749  recexpr  7753  aptiprleml  7754  archpr  7758  cauappcvgprlemm  7760  cauappcvgprlemloc  7767  cauappcvgprlem1  7774  cauappcvgprlem2  7775  cauappcvgpr  7777  caucvgprlemm  7783  caucvgprlemloc  7790  caucvgprlem1  7794  caucvgprlem2  7795  caucvgpr  7797  caucvgprprlemmu  7810  caucvgprprlemopl  7812  caucvgprprlemopu  7814  caucvgprprlemloc  7818  caucvgprprlem1  7824  caucvgprprlem2  7825  caucvgprpr  7827  suplocexprlemmu  7833  suplocexprlemloc  7836  suplocexpr  7840  negexsr  7887  recexgt0sr  7888  caucvgsrlemgt1  7910  caucvgsrlemoffres  7915  suplocsrlem  7923  axrnegex  7994  axprecex  7995  nntopi  8009  axcaucvglemres  8014  axpre-suploclemres  8016  cnegex  8252  recexre  8653  recexap  8728  receuap  8744  rerecapb  8918  sup3exmid  9032  cju  9036  nn2ge  9071  nominpos  9277  zdiv  9463  btwnz  9494  supinfneg  9718  infsupneg  9719  ublbneg  9736  lbzbi  9739  zq  9749  z2ge  9950  iccsupr  10090  zsupcllemstep  10374  infssuzex  10378  suprzubdc  10381  zsupssdc  10383  exbtwnzlemstep  10392  exbtwnzlemex  10394  rebtwn2zlemstep  10397  rebtwn2z  10399  qbtwnre  10401  qbtwnxr  10402  expnbnd  10810  hashunlem  10951  iswrdinn0  11001  shftlem  11160  shftfvalg  11162  shftfval  11165  caucvgre  11325  cvg1nlemres  11329  rexanuz  11332  rexuz3  11334  resqrexlemex  11369  caubnd2  11461  maxabslemval  11552  maxleast  11557  rexanre  11564  rexico  11565  fimaxre2  11571  minmax  11574  xrmaxiflemval  11594  xrmaxaddlem  11604  xrminmax  11609  climconst  11634  climshftlemg  11646  cn1lem  11658  serf0  11696  zsumdc  11728  fsum3  11731  fsum3cvg3  11740  mertenslemi1  11879  ntrivcvgap0  11893  zproddc  11923  fprodseq  11927  fprodntrivap  11928  dvdsval2  12134  dvds0lem  12145  dvds1lem  12146  dvds2lem  12147  odd2np1lem  12216  odd2np1  12217  opeo  12241  omeo  12242  divalglemex  12266  bezoutlemnewy  12350  bezoutlemaz  12357  bezoutlembz  12358  bezoutlemsup  12363  nnwodc  12390  uzwodc  12391  ncoprmgcdne1b  12444  exprmfct  12493  reumodprminv  12609  modprm0  12610  nnnn0modprm0  12611  pythagtriplem19  12638  pcprmpw2  12689  pockthi  12714  infpnlem2  12716  ennnfonelemex  12818  ennnfonelemhom  12819  ennnfonelemrn  12823  ennnfonelemnn0  12826  ennnfonelemim  12828  exmidunben  12830  ctinfomlemom  12831  ctinfom  12832  ctinf  12834  ctiunctlemf  12842  ismgmid2  13245  mgmidsssn0  13249  ismndd  13302  isgrpd2  13386  isgrpd  13388  imasgrp2  13479  mhmmnd  13485  ghmgrp  13487  dvdsrmuld  13891  dvdsr01  13899  rhmdvdsr  13970  lspf  14184  lspval  14185  lssats2  14209  fiinbas  14554  topbas  14572  clsval  14616  neiint  14650  neipsm  14659  opnneissb  14660  opnssneib  14661  innei  14668  restbasg  14673  lmconst  14721  iscnp4  14723  cncnpi  14733  cnconst2  14738  cnptoprest  14744  cnpdis  14747  neitx  14773  txcnp  14776  blssps  14932  blss  14933  blssexps  14934  blssex  14935  ssblex  14936  blin2  14937  neibl  14996  metss2  15003  bdmopn  15009  metrest  15011  metcnp3  15016  tgioo  15059  tgqioo  15060  addcncntoplem  15066  cnopnap  15116  dedekindeulemuub  15122  suplociccreex  15129  dedekindicclemuub  15131  ivthinclemlm  15139  ivthinclemum  15140  ivthinclemlopn  15141  ivthinclemuopn  15143  ivthreinc  15150  elply2  15240  reeff1oleme  15277  sin0pilem2  15287  sgmnncl  15493  dvdsppwf1o  15494  perfect  15506  bj-nn0suc0  15923  bj-inf2vnlem1  15943  nninfsellemeq  15988  nninfomnilem  15992  qdencn  16003  trirec0  16020