Theorem rspcev 2825

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1342   e. wcel 2135   E.wrex 2443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-rex 2448  df-v 2723

This theorem is referenced by:  rspceaimv  2833  rspc2ev  2840  rspc3ev  2842  rspceeqv  2843  reu6i  2912  rspesbca  3030  brralrspcev  4034  nn0suc  4575  elrnmpt1s  4848  elrnrexdm  5618  eldmrexrn  5620  foco2  5716  elabrex  5720  f1elima  5735  fcofo  5746  fliftfun  5758  fliftval  5762  f1oiso2  5789  fo1st  6117  fo2nd  6118  tfr0dm  6281  tfrlemisucaccv  6284  tfrlemi14d  6292  tfrexlem  6293  tfr1onlemsucaccv  6300  tfr1onlemres  6308  tfrcllemsucaccv  6313  tfrcllemres  6321  rdgss  6342  frecabcl  6358  nnaordex  6486  nnawordex  6487  ecelqsg  6545  snfig  6771  nnfi  6829  findcard  6845  fimax2gtrilemstep  6857  unsnfi  6875  eqsupti  6952  supmaxti  6960  supisoex  6965  infminti  6983  finomni  7095  isnumi  7129  oncardval  7133  archnqq  7349  prarloclemarch2  7351  prcdnql  7416  prcunqu  7417  prarloclemlo  7426  prarloclem5  7432  nqprm  7474  1idprl  7522  1idpru  7523  ltexpri  7545  prplnqu  7552  recexprlemm  7556  recexprlem1ssl  7565  recexprlem1ssu  7566  recexpr  7570  aptiprleml  7571  archpr  7575  cauappcvgprlemm  7577  cauappcvgprlemloc  7584  cauappcvgprlem1  7591  cauappcvgprlem2  7592  cauappcvgpr  7594  caucvgprlemm  7600  caucvgprlemloc  7607  caucvgprlem1  7611  caucvgprlem2  7612  caucvgpr  7614  caucvgprprlemmu  7627  caucvgprprlemopl  7629  caucvgprprlemopu  7631  caucvgprprlemloc  7635  caucvgprprlem1  7641  caucvgprprlem2  7642  caucvgprpr  7644  suplocexprlemmu  7650  suplocexprlemloc  7653  suplocexpr  7657  negexsr  7704  recexgt0sr  7705  caucvgsrlemgt1  7727  caucvgsrlemoffres  7732  suplocsrlem  7740  axrnegex  7811  axprecex  7812  nntopi  7826  axcaucvglemres  7831  axpre-suploclemres  7833  cnegex  8067  recexre  8467  recexap  8541  receuap  8557  sup3exmid  8843  cju  8847  nn2ge  8881  nominpos  9085  zdiv  9270  btwnz  9301  supinfneg  9524  infsupneg  9525  ublbneg  9542  lbzbi  9545  zq  9555  z2ge  9753  iccsupr  9893  exbtwnzlemstep  10173  exbtwnzlemex  10175  rebtwn2zlemstep  10178  rebtwn2z  10180  qbtwnre  10182  qbtwnxr  10183  expnbnd  10567  hashunlem  10706  shftlem  10744  shftfvalg  10746  shftfval  10749  caucvgre  10909  cvg1nlemres  10913  rexanuz  10916  rexuz3  10918  resqrexlemex  10953  caubnd2  11045  maxabslemval  11136  maxleast  11141  rexanre  11148  rexico  11149  fimaxre2  11154  minmax  11157  xrmaxiflemval  11177  xrmaxaddlem  11187  xrminmax  11192  climconst  11217  climshftlemg  11229  cn1lem  11241  serf0  11279  zsumdc  11311  fsum3  11314  fsum3cvg3  11323  mertenslemi1  11462  ntrivcvgap0  11476  zproddc  11506  fprodseq  11510  fprodntrivap  11511  dvdsval2  11716  dvds0lem  11727  dvds1lem  11728  dvds2lem  11729  odd2np1lem  11794  odd2np1  11795  opeo  11819  omeo  11820  divalglemex  11844  zsupcllemstep  11863  infssuzex  11867  suprzubdc  11870  zsupssdc  11872  bezoutlemnewy  11914  bezoutlemaz  11921  bezoutlembz  11922  bezoutlemsup  11927  ncoprmgcdne1b  12000  exprmfct  12049  reumodprminv  12162  modprm0  12163  nnnn0modprm0  12164  pythagtriplem19  12191  pcprmpw2  12241  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemrn  12289  ennnfonelemnn0  12292  ennnfonelemim  12294  exmidunben  12296  ctinfomlemom  12297  ctinfom  12298  ctinf  12300  ctiunctlemf  12308  fiinbas  12588  topbas  12608  clsval  12652  neiint  12686  neipsm  12695  opnneissb  12696  opnssneib  12697  innei  12704  restbasg  12709  lmconst  12757  iscnp4  12759  cncnpi  12769  cnconst2  12774  cnptoprest  12780  cnpdis  12783  neitx  12809  txcnp  12812  blssps  12968  blss  12969  blssexps  12970  blssex  12971  ssblex  12972  blin2  12973  neibl  13032  metss2  13039  bdmopn  13045  metrest  13047  metcnp3  13052  tgioo  13087  tgqioo  13088  addcncntoplem  13092  cnopnap  13135  dedekindeulemuub  13136  suplociccreex  13143  dedekindicclemuub  13145  ivthinclemlm  13153  ivthinclemum  13154  ivthinclemlopn  13155  ivthinclemuopn  13157  reeff1oleme  13234  sin0pilem2  13244  bj-nn0suc0  13667  bj-inf2vnlem1  13687  nninfsellemeq  13728  nninfomnilem  13732  qdencn  13740  trirec0  13757