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  4102  nn0suc  4652  elrnmpt1s  4928  elrnrexdm  5719  eldmrexrn  5721  foco2  5822  elabrex  5826  elabrexg  5827  f1elima  5842  fcofo  5853  fliftfun  5865  fliftval  5869  f1oiso2  5896  fo1st  6243  fo2nd  6244  tfr0dm  6408  tfrlemisucaccv  6411  tfrlemi14d  6419  tfrexlem  6420  tfr1onlemsucaccv  6427  tfr1onlemres  6435  tfrcllemsucaccv  6440  tfrcllemres  6448  rdgss  6469  frecabcl  6485  nnaordex  6614  nnawordex  6615  ecelqsg  6675  snfig  6906  nnfi  6969  findcard  6985  fimax2gtrilemstep  6997  unsnfi  7016  eqsupti  7098  supmaxti  7106  supisoex  7111  infminti  7129  finomni  7242  nninfwlpoimlemginf  7278  isnumi  7289  oncardval  7293  archnqq  7530  prarloclemarch2  7532  prcdnql  7597  prcunqu  7598  prarloclemlo  7607  prarloclem5  7613  nqprm  7655  1idprl  7703  1idpru  7704  ltexpri  7726  prplnqu  7733  recexprlemm  7737  recexprlem1ssl  7746  recexprlem1ssu  7747  recexpr  7751  aptiprleml  7752  archpr  7756  cauappcvgprlemm  7758  cauappcvgprlemloc  7765  cauappcvgprlem1  7772  cauappcvgprlem2  7773  cauappcvgpr  7775  caucvgprlemm  7781  caucvgprlemloc  7788  caucvgprlem1  7792  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgprpr  7825  suplocexprlemmu  7831  suplocexprlemloc  7834  suplocexpr  7838  negexsr  7885  recexgt0sr  7886  caucvgsrlemgt1  7908  caucvgsrlemoffres  7913  suplocsrlem  7921  axrnegex  7992  axprecex  7993  nntopi  8007  axcaucvglemres  8012  axpre-suploclemres  8014  cnegex  8250  recexre  8651  recexap  8726  receuap  8742  rerecapb  8916  sup3exmid  9030  cju  9034  nn2ge  9069  nominpos  9275  zdiv  9461  btwnz  9492  supinfneg  9716  infsupneg  9717  ublbneg  9734  lbzbi  9737  zq  9747  z2ge  9948  iccsupr  10088  zsupcllemstep  10372  infssuzex  10376  suprzubdc  10379  zsupssdc  10381  exbtwnzlemstep  10390  exbtwnzlemex  10392  rebtwn2zlemstep  10395  rebtwn2z  10397  qbtwnre  10399  qbtwnxr  10400  expnbnd  10808  hashunlem  10949  iswrdinn0  10999  shftlem  11127  shftfvalg  11129  shftfval  11132  caucvgre  11292  cvg1nlemres  11296  rexanuz  11299  rexuz3  11301  resqrexlemex  11336  caubnd2  11428  maxabslemval  11519  maxleast  11524  rexanre  11531  rexico  11532  fimaxre2  11538  minmax  11541  xrmaxiflemval  11561  xrmaxaddlem  11571  xrminmax  11576  climconst  11601  climshftlemg  11613  cn1lem  11625  serf0  11663  zsumdc  11695  fsum3  11698  fsum3cvg3  11707  mertenslemi1  11846  ntrivcvgap0  11860  zproddc  11890  fprodseq  11894  fprodntrivap  11895  dvdsval2  12101  dvds0lem  12112  dvds1lem  12113  dvds2lem  12114  odd2np1lem  12183  odd2np1  12184  opeo  12208  omeo  12209  divalglemex  12233  bezoutlemnewy  12317  bezoutlemaz  12324  bezoutlembz  12325  bezoutlemsup  12330  nnwodc  12357  uzwodc  12358  ncoprmgcdne1b  12411  exprmfct  12460  reumodprminv  12576  modprm0  12577  nnnn0modprm0  12578  pythagtriplem19  12605  pcprmpw2  12656  pockthi  12681  infpnlem2  12683  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemrn  12790  ennnfonelemnn0  12793  ennnfonelemim  12795  exmidunben  12797  ctinfomlemom  12798  ctinfom  12799  ctinf  12801  ctiunctlemf  12809  ismgmid2  13212  mgmidsssn0  13216  ismndd  13269  isgrpd2  13353  isgrpd  13355  imasgrp2  13446  mhmmnd  13452  ghmgrp  13454  dvdsrmuld  13858  dvdsr01  13866  rhmdvdsr  13937  lspf  14151  lspval  14152  lssats2  14176  fiinbas  14521  topbas  14539  clsval  14583  neiint  14617  neipsm  14626  opnneissb  14627  opnssneib  14628  innei  14635  restbasg  14640  lmconst  14688  iscnp4  14690  cncnpi  14700  cnconst2  14705  cnptoprest  14711  cnpdis  14714  neitx  14740  txcnp  14743  blssps  14899  blss  14900  blssexps  14901  blssex  14902  ssblex  14903  blin2  14904  neibl  14963  metss2  14970  bdmopn  14976  metrest  14978  metcnp3  14983  tgioo  15026  tgqioo  15027  addcncntoplem  15033  cnopnap  15083  dedekindeulemuub  15089  suplociccreex  15096  dedekindicclemuub  15098  ivthinclemlm  15106  ivthinclemum  15107  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthreinc  15117  elply2  15207  reeff1oleme  15244  sin0pilem2  15254  sgmnncl  15460  dvdsppwf1o  15461  perfect  15473  bj-nn0suc0  15890  bj-inf2vnlem1  15910  nninfsellemeq  15955  nninfomnilem  15959  qdencn  15970  trirec0  15987