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  7238  supmaxti  7246  supisoex  7251  infminti  7269  finomni  7382  nninfwlpoimlemginf  7418  isnumi  7429  oncardval  7433  archnqq  7680  prarloclemarch2  7682  prcdnql  7747  prcunqu  7748  prarloclemlo  7757  prarloclem5  7763  nqprm  7805  1idprl  7853  1idpru  7854  ltexpri  7876  prplnqu  7883  recexprlemm  7887  recexprlem1ssl  7896  recexprlem1ssu  7897  recexpr  7901  aptiprleml  7902  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemloc  7915  cauappcvgprlem1  7922  cauappcvgprlem2  7923  cauappcvgpr  7925  caucvgprlemm  7931  caucvgprlemloc  7938  caucvgprlem1  7942  caucvgprlem2  7943  caucvgpr  7945  caucvgprprlemmu  7958  caucvgprprlemopl  7960  caucvgprprlemopu  7962  caucvgprprlemloc  7966  caucvgprprlem1  7972  caucvgprprlem2  7973  caucvgprpr  7975  suplocexprlemmu  7981  suplocexprlemloc  7984  suplocexpr  7988  negexsr  8035  recexgt0sr  8036  caucvgsrlemgt1  8058  caucvgsrlemoffres  8063  suplocsrlem  8071  axrnegex  8142  axprecex  8143  nntopi  8157  axcaucvglemres  8162  axpre-suploclemres  8164  cnegex  8400  recexre  8801  recexap  8876  receuap  8892  rerecapb  9066  sup3exmid  9180  cju  9184  nn2ge  9219  nominpos  9425  zdiv  9611  btwnz  9642  supinfneg  9872  infsupneg  9873  ublbneg  9890  lbzbi  9893  zq  9903  z2ge  10104  iccsupr  10244  zsupcllemstep  10533  infssuzex  10537  suprzubdc  10540  zsupssdc  10542  exbtwnzlemstep  10551  exbtwnzlemex  10553  rebtwn2zlemstep  10556  rebtwn2z  10558  qbtwnre  10560  qbtwnxr  10561  expnbnd  10969  hashunlem  11111  iswrdinn0  11165  shftlem  11437  shftfvalg  11439  shftfval  11442  caucvgre  11602  cvg1nlemres  11606  rexanuz  11609  rexuz3  11611  resqrexlemex  11646  caubnd2  11738  maxabslemval  11829  maxleast  11834  rexanre  11841  rexico  11842  fimaxre2  11848  minmax  11851  xrmaxiflemval  11871  xrmaxaddlem  11881  xrminmax  11886  climconst  11911  climshftlemg  11923  cn1lem  11935  serf0  11973  zsumdc  12006  fsum3  12009  fsum3cvg3  12018  mertenslemi1  12157  ntrivcvgap0  12171  zproddc  12201  fprodseq  12205  fprodntrivap  12206  dvdsval2  12412  dvds0lem  12423  dvds1lem  12424  dvds2lem  12425  odd2np1lem  12494  odd2np1  12495  opeo  12519  omeo  12520  divalglemex  12544  bezoutlemnewy  12628  bezoutlemaz  12635  bezoutlembz  12636  bezoutlemsup  12641  nnwodc  12668  uzwodc  12669  ncoprmgcdne1b  12722  exprmfct  12771  reumodprminv  12887  modprm0  12888  nnnn0modprm0  12889  pythagtriplem19  12916  pcprmpw2  12967  pockthi  12992  infpnlem2  12994  ennnfonelemex  13096  ennnfonelemhom  13097  ennnfonelemrn  13101  ennnfonelemnn0  13104  ennnfonelemim  13106  exmidunben  13108  ctinfomlemom  13109  ctinfom  13110  ctinf  13112  ctiunctlemf  13120  ismgmid2  13524  mgmidsssn0  13528  ismndd  13581  isgrpd2  13665  isgrpd  13667  imasgrp2  13758  mhmmnd  13764  ghmgrp  13766  dvdsrmuld  14172  dvdsr01  14180  rhmdvdsr  14251  lspf  14465  lspval  14466  lssats2  14490  fiinbas  14840  topbas  14858  clsval  14902  neiint  14936  neipsm  14945  opnneissb  14946  opnssneib  14947  innei  14954  restbasg  14959  lmconst  15007  iscnp4  15009  cncnpi  15019  cnconst2  15024  cnptoprest  15030  cnpdis  15033  neitx  15059  txcnp  15062  blssps  15218  blss  15219  blssexps  15220  blssex  15221  ssblex  15222  blin2  15223  neibl  15282  metss2  15289  bdmopn  15295  metrest  15297  metcnp3  15302  tgioo  15345  tgqioo  15346  addcncntoplem  15352  cnopnap  15402  dedekindeulemuub  15408  suplociccreex  15415  dedekindicclemuub  15417  ivthinclemlm  15425  ivthinclemum  15426  ivthinclemlopn  15427  ivthinclemuopn  15429  ivthreinc  15436  elply2  15526  reeff1oleme  15563  sin0pilem2  15573  sgmnncl  15779  dvdsppwf1o  15780  perfect  15792  bj-nn0suc0  16643  bj-inf2vnlem1  16663  3dom  16685  nninfsellemeq  16717  nninfomnilem  16721  qdencn  16732  trirec0  16753  qdiff  16758