Theorem rspcev 2834

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   e. wcel 2141   E.wrex 2449

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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732

This theorem is referenced by:  rspceaimv  2842  rspc2ev  2849  rspc3ev  2851  rspceeqv  2852  reu6i  2921  rspesbca  3039  brralrspcev  4045  nn0suc  4586  elrnmpt1s  4859  elrnrexdm  5633  eldmrexrn  5635  foco2  5731  elabrex  5735  f1elima  5750  fcofo  5761  fliftfun  5773  fliftval  5777  f1oiso2  5804  fo1st  6134  fo2nd  6135  tfr0dm  6299  tfrlemisucaccv  6302  tfrlemi14d  6310  tfrexlem  6311  tfr1onlemsucaccv  6318  tfr1onlemres  6326  tfrcllemsucaccv  6331  tfrcllemres  6339  rdgss  6360  frecabcl  6376  nnaordex  6504  nnawordex  6505  ecelqsg  6563  snfig  6789  nnfi  6847  findcard  6863  fimax2gtrilemstep  6875  unsnfi  6893  eqsupti  6970  supmaxti  6978  supisoex  6983  infminti  7001  finomni  7113  isnumi  7148  oncardval  7152  archnqq  7368  prarloclemarch2  7370  prcdnql  7435  prcunqu  7436  prarloclemlo  7445  prarloclem5  7451  nqprm  7493  1idprl  7541  1idpru  7542  ltexpri  7564  prplnqu  7571  recexprlemm  7575  recexprlem1ssl  7584  recexprlem1ssu  7585  recexpr  7589  aptiprleml  7590  archpr  7594  cauappcvgprlemm  7596  cauappcvgprlemloc  7603  cauappcvgprlem1  7610  cauappcvgprlem2  7611  cauappcvgpr  7613  caucvgprlemm  7619  caucvgprlemloc  7626  caucvgprlem1  7630  caucvgprlem2  7631  caucvgpr  7633  caucvgprprlemmu  7646  caucvgprprlemopl  7648  caucvgprprlemopu  7650  caucvgprprlemloc  7654  caucvgprprlem1  7660  caucvgprprlem2  7661  caucvgprpr  7663  suplocexprlemmu  7669  suplocexprlemloc  7672  suplocexpr  7676  negexsr  7723  recexgt0sr  7724  caucvgsrlemgt1  7746  caucvgsrlemoffres  7751  suplocsrlem  7759  axrnegex  7830  axprecex  7831  nntopi  7845  axcaucvglemres  7850  axpre-suploclemres  7852  cnegex  8086  recexre  8486  recexap  8560  receuap  8576  sup3exmid  8862  cju  8866  nn2ge  8900  nominpos  9104  zdiv  9289  btwnz  9320  supinfneg  9543  infsupneg  9544  ublbneg  9561  lbzbi  9564  zq  9574  z2ge  9772  iccsupr  9912  exbtwnzlemstep  10193  exbtwnzlemex  10195  rebtwn2zlemstep  10198  rebtwn2z  10200  qbtwnre  10202  qbtwnxr  10203  expnbnd  10588  hashunlem  10728  shftlem  10769  shftfvalg  10771  shftfval  10774  caucvgre  10934  cvg1nlemres  10938  rexanuz  10941  rexuz3  10943  resqrexlemex  10978  caubnd2  11070  maxabslemval  11161  maxleast  11166  rexanre  11173  rexico  11174  fimaxre2  11179  minmax  11182  xrmaxiflemval  11202  xrmaxaddlem  11212  xrminmax  11217  climconst  11242  climshftlemg  11254  cn1lem  11266  serf0  11304  zsumdc  11336  fsum3  11339  fsum3cvg3  11348  mertenslemi1  11487  ntrivcvgap0  11501  zproddc  11531  fprodseq  11535  fprodntrivap  11536  dvdsval2  11741  dvds0lem  11752  dvds1lem  11753  dvds2lem  11754  odd2np1lem  11820  odd2np1  11821  opeo  11845  omeo  11846  divalglemex  11870  zsupcllemstep  11889  infssuzex  11893  suprzubdc  11896  zsupssdc  11898  bezoutlemnewy  11940  bezoutlemaz  11947  bezoutlembz  11948  bezoutlemsup  11953  nnwodc  11980  uzwodc  11981  ncoprmgcdne1b  12032  exprmfct  12081  reumodprminv  12196  modprm0  12197  nnnn0modprm0  12198  pythagtriplem19  12225  pcprmpw2  12275  pockthi  12299  infpnlem2  12301  ennnfonelemex  12358  ennnfonelemhom  12359  ennnfonelemrn  12363  ennnfonelemnn0  12366  ennnfonelemim  12368  exmidunben  12370  ctinfomlemom  12371  ctinfom  12372  ctinf  12374  ctiunctlemf  12382  ismgmid2  12623  mgmidsssn0  12627  ismndd  12662  isgrpd2  12716  isgrpd  12718  fiinbas  12802  topbas  12822  clsval  12866  neiint  12900  neipsm  12909  opnneissb  12910  opnssneib  12911  innei  12918  restbasg  12923  lmconst  12971  iscnp4  12973  cncnpi  12983  cnconst2  12988  cnptoprest  12994  cnpdis  12997  neitx  13023  txcnp  13026  blssps  13182  blss  13183  blssexps  13184  blssex  13185  ssblex  13186  blin2  13187  neibl  13246  metss2  13253  bdmopn  13259  metrest  13261  metcnp3  13266  tgioo  13301  tgqioo  13302  addcncntoplem  13306  cnopnap  13349  dedekindeulemuub  13350  suplociccreex  13357  dedekindicclemuub  13359  ivthinclemlm  13367  ivthinclemum  13368  ivthinclemlopn  13369  ivthinclemuopn  13371  reeff1oleme  13448  sin0pilem2  13458  bj-nn0suc0  13947  bj-inf2vnlem1  13967  nninfsellemeq  14009  nninfomnilem  14013  qdencn  14021  trirec0  14038