Theorem rspcev 2841

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   E.wrex 2456

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739

This theorem is referenced by:  rspceaimv  2849  rspc2ev  2856  rspc3ev  2858  rspceeqv  2859  reu6i  2928  rspesbca  3047  brralrspcev  4059  nn0suc  4601  elrnmpt1s  4874  elrnrexdm  5652  eldmrexrn  5654  foco2  5750  elabrex  5754  f1elima  5769  fcofo  5780  fliftfun  5792  fliftval  5796  f1oiso2  5823  fo1st  6153  fo2nd  6154  tfr0dm  6318  tfrlemisucaccv  6321  tfrlemi14d  6329  tfrexlem  6330  tfr1onlemsucaccv  6337  tfr1onlemres  6345  tfrcllemsucaccv  6350  tfrcllemres  6358  rdgss  6379  frecabcl  6395  nnaordex  6524  nnawordex  6525  ecelqsg  6583  snfig  6809  nnfi  6867  findcard  6883  fimax2gtrilemstep  6895  unsnfi  6913  eqsupti  6990  supmaxti  6998  supisoex  7003  infminti  7021  finomni  7133  nninfwlpoimlemginf  7169  isnumi  7176  oncardval  7180  archnqq  7411  prarloclemarch2  7413  prcdnql  7478  prcunqu  7479  prarloclemlo  7488  prarloclem5  7494  nqprm  7536  1idprl  7584  1idpru  7585  ltexpri  7607  prplnqu  7614  recexprlemm  7618  recexprlem1ssl  7627  recexprlem1ssu  7628  recexpr  7632  aptiprleml  7633  archpr  7637  cauappcvgprlemm  7639  cauappcvgprlemloc  7646  cauappcvgprlem1  7653  cauappcvgprlem2  7654  cauappcvgpr  7656  caucvgprlemm  7662  caucvgprlemloc  7669  caucvgprlem1  7673  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlem1  7703  caucvgprprlem2  7704  caucvgprpr  7706  suplocexprlemmu  7712  suplocexprlemloc  7715  suplocexpr  7719  negexsr  7766  recexgt0sr  7767  caucvgsrlemgt1  7789  caucvgsrlemoffres  7794  suplocsrlem  7802  axrnegex  7873  axprecex  7874  nntopi  7888  axcaucvglemres  7893  axpre-suploclemres  7895  cnegex  8129  recexre  8529  recexap  8604  receuap  8620  rerecapb  8794  sup3exmid  8908  cju  8912  nn2ge  8946  nominpos  9150  zdiv  9335  btwnz  9366  supinfneg  9589  infsupneg  9590  ublbneg  9607  lbzbi  9610  zq  9620  z2ge  9820  iccsupr  9960  exbtwnzlemstep  10241  exbtwnzlemex  10243  rebtwn2zlemstep  10246  rebtwn2z  10248  qbtwnre  10250  qbtwnxr  10251  expnbnd  10636  hashunlem  10775  shftlem  10816  shftfvalg  10818  shftfval  10821  caucvgre  10981  cvg1nlemres  10985  rexanuz  10988  rexuz3  10990  resqrexlemex  11025  caubnd2  11117  maxabslemval  11208  maxleast  11213  rexanre  11220  rexico  11221  fimaxre2  11226  minmax  11229  xrmaxiflemval  11249  xrmaxaddlem  11259  xrminmax  11264  climconst  11289  climshftlemg  11301  cn1lem  11313  serf0  11351  zsumdc  11383  fsum3  11386  fsum3cvg3  11395  mertenslemi1  11534  ntrivcvgap0  11548  zproddc  11578  fprodseq  11582  fprodntrivap  11583  dvdsval2  11788  dvds0lem  11799  dvds1lem  11800  dvds2lem  11801  odd2np1lem  11867  odd2np1  11868  opeo  11892  omeo  11893  divalglemex  11917  zsupcllemstep  11936  infssuzex  11940  suprzubdc  11943  zsupssdc  11945  bezoutlemnewy  11987  bezoutlemaz  11994  bezoutlembz  11995  bezoutlemsup  12000  nnwodc  12027  uzwodc  12028  ncoprmgcdne1b  12079  exprmfct  12128  reumodprminv  12243  modprm0  12244  nnnn0modprm0  12245  pythagtriplem19  12272  pcprmpw2  12322  pockthi  12346  infpnlem2  12348  ennnfonelemex  12405  ennnfonelemhom  12406  ennnfonelemrn  12410  ennnfonelemnn0  12413  ennnfonelemim  12415  exmidunben  12417  ctinfomlemom  12418  ctinfom  12419  ctinf  12421  ctiunctlemf  12429  ismgmid2  12729  mgmidsssn0  12733  ismndd  12768  isgrpd2  12825  isgrpd  12827  mhmmnd  12908  ghmgrp  12910  dvdsrmuld  13164  dvdsr01  13172  fiinbas  13329  topbas  13349  clsval  13393  neiint  13427  neipsm  13436  opnneissb  13437  opnssneib  13438  innei  13445  restbasg  13450  lmconst  13498  iscnp4  13500  cncnpi  13510  cnconst2  13515  cnptoprest  13521  cnpdis  13524  neitx  13550  txcnp  13553  blssps  13709  blss  13710  blssexps  13711  blssex  13712  ssblex  13713  blin2  13714  neibl  13773  metss2  13780  bdmopn  13786  metrest  13788  metcnp3  13793  tgioo  13828  tgqioo  13829  addcncntoplem  13833  cnopnap  13876  dedekindeulemuub  13877  suplociccreex  13884  dedekindicclemuub  13886  ivthinclemlm  13894  ivthinclemum  13895  ivthinclemlopn  13896  ivthinclemuopn  13898  reeff1oleme  13975  sin0pilem2  13985  bj-nn0suc0  14473  bj-inf2vnlem1  14493  nninfsellemeq  14534  nninfomnilem  14538  qdencn  14546  trirec0  14563