Theorem rspcev 2907

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   E.wrex 2509

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801

This theorem is referenced by:  rspceaimv  2915  rspc2ev  2922  rspc3ev  2924  rspceeqv  2925  reu6i  2994  rspesbca  3114  brralrspcev  4142  nn0suc  4696  elrnmpt1s  4974  elrnrexdm  5774  eldmrexrn  5776  foco2  5877  elabrex  5881  elabrexg  5882  f1elima  5897  fcofo  5908  fliftfun  5920  fliftval  5924  f1oiso2  5951  fo1st  6303  fo2nd  6304  tfr0dm  6468  tfrlemisucaccv  6471  tfrlemi14d  6479  tfrexlem  6480  tfr1onlemsucaccv  6487  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllemres  6508  rdgss  6529  frecabcl  6545  nnaordex  6674  nnawordex  6675  ecelqsg  6735  snfig  6967  nnfi  7034  findcard  7050  fimax2gtrilemstep  7062  unsnfi  7081  eqsupti  7163  supmaxti  7171  supisoex  7176  infminti  7194  finomni  7307  nninfwlpoimlemginf  7343  isnumi  7354  oncardval  7358  archnqq  7604  prarloclemarch2  7606  prcdnql  7671  prcunqu  7672  prarloclemlo  7681  prarloclem5  7687  nqprm  7729  1idprl  7777  1idpru  7778  ltexpri  7800  prplnqu  7807  recexprlemm  7811  recexprlem1ssl  7820  recexprlem1ssu  7821  recexpr  7825  aptiprleml  7826  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemloc  7839  cauappcvgprlem1  7846  cauappcvgprlem2  7847  cauappcvgpr  7849  caucvgprlemm  7855  caucvgprlemloc  7862  caucvgprlem1  7866  caucvgprlem2  7867  caucvgpr  7869  caucvgprprlemmu  7882  caucvgprprlemopl  7884  caucvgprprlemopu  7886  caucvgprprlemloc  7890  caucvgprprlem1  7896  caucvgprprlem2  7897  caucvgprpr  7899  suplocexprlemmu  7905  suplocexprlemloc  7908  suplocexpr  7912  negexsr  7959  recexgt0sr  7960  caucvgsrlemgt1  7982  caucvgsrlemoffres  7987  suplocsrlem  7995  axrnegex  8066  axprecex  8067  nntopi  8081  axcaucvglemres  8086  axpre-suploclemres  8088  cnegex  8324  recexre  8725  recexap  8800  receuap  8816  rerecapb  8990  sup3exmid  9104  cju  9108  nn2ge  9143  nominpos  9349  zdiv  9535  btwnz  9566  supinfneg  9790  infsupneg  9791  ublbneg  9808  lbzbi  9811  zq  9821  z2ge  10022  iccsupr  10162  zsupcllemstep  10449  infssuzex  10453  suprzubdc  10456  zsupssdc  10458  exbtwnzlemstep  10467  exbtwnzlemex  10469  rebtwn2zlemstep  10472  rebtwn2z  10474  qbtwnre  10476  qbtwnxr  10477  expnbnd  10885  hashunlem  11026  iswrdinn0  11076  shftlem  11327  shftfvalg  11329  shftfval  11332  caucvgre  11492  cvg1nlemres  11496  rexanuz  11499  rexuz3  11501  resqrexlemex  11536  caubnd2  11628  maxabslemval  11719  maxleast  11724  rexanre  11731  rexico  11732  fimaxre2  11738  minmax  11741  xrmaxiflemval  11761  xrmaxaddlem  11771  xrminmax  11776  climconst  11801  climshftlemg  11813  cn1lem  11825  serf0  11863  zsumdc  11895  fsum3  11898  fsum3cvg3  11907  mertenslemi1  12046  ntrivcvgap0  12060  zproddc  12090  fprodseq  12094  fprodntrivap  12095  dvdsval2  12301  dvds0lem  12312  dvds1lem  12313  dvds2lem  12314  odd2np1lem  12383  odd2np1  12384  opeo  12408  omeo  12409  divalglemex  12433  bezoutlemnewy  12517  bezoutlemaz  12524  bezoutlembz  12525  bezoutlemsup  12530  nnwodc  12557  uzwodc  12558  ncoprmgcdne1b  12611  exprmfct  12660  reumodprminv  12776  modprm0  12777  nnnn0modprm0  12778  pythagtriplem19  12805  pcprmpw2  12856  pockthi  12881  infpnlem2  12883  ennnfonelemex  12985  ennnfonelemhom  12986  ennnfonelemrn  12990  ennnfonelemnn0  12993  ennnfonelemim  12995  exmidunben  12997  ctinfomlemom  12998  ctinfom  12999  ctinf  13001  ctiunctlemf  13009  ismgmid2  13413  mgmidsssn0  13417  ismndd  13470  isgrpd2  13554  isgrpd  13556  imasgrp2  13647  mhmmnd  13653  ghmgrp  13655  dvdsrmuld  14060  dvdsr01  14068  rhmdvdsr  14139  lspf  14353  lspval  14354  lssats2  14378  fiinbas  14723  topbas  14741  clsval  14785  neiint  14819  neipsm  14828  opnneissb  14829  opnssneib  14830  innei  14837  restbasg  14842  lmconst  14890  iscnp4  14892  cncnpi  14902  cnconst2  14907  cnptoprest  14913  cnpdis  14916  neitx  14942  txcnp  14945  blssps  15101  blss  15102  blssexps  15103  blssex  15104  ssblex  15105  blin2  15106  neibl  15165  metss2  15172  bdmopn  15178  metrest  15180  metcnp3  15185  tgioo  15228  tgqioo  15229  addcncntoplem  15235  cnopnap  15285  dedekindeulemuub  15291  suplociccreex  15298  dedekindicclemuub  15300  ivthinclemlm  15308  ivthinclemum  15309  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthreinc  15319  elply2  15409  reeff1oleme  15446  sin0pilem2  15456  sgmnncl  15662  dvdsppwf1o  15663  perfect  15675  bj-nn0suc0  16313  bj-inf2vnlem1  16333  nninfsellemeq  16380  nninfomnilem  16384  qdencn  16395  trirec0  16412