Theorem rspcev 2865

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   e. wcel 2164   E.wrex 2473

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762

This theorem is referenced by:  rspceaimv  2873  rspc2ev  2880  rspc3ev  2882  rspceeqv  2883  reu6i  2952  rspesbca  3071  brralrspcev  4088  nn0suc  4637  elrnmpt1s  4913  elrnrexdm  5698  eldmrexrn  5700  foco2  5797  elabrex  5801  elabrexg  5802  f1elima  5817  fcofo  5828  fliftfun  5840  fliftval  5844  f1oiso2  5871  fo1st  6212  fo2nd  6213  tfr0dm  6377  tfrlemisucaccv  6380  tfrlemi14d  6388  tfrexlem  6389  tfr1onlemsucaccv  6396  tfr1onlemres  6404  tfrcllemsucaccv  6409  tfrcllemres  6417  rdgss  6438  frecabcl  6454  nnaordex  6583  nnawordex  6584  ecelqsg  6644  snfig  6870  nnfi  6930  findcard  6946  fimax2gtrilemstep  6958  unsnfi  6977  eqsupti  7057  supmaxti  7065  supisoex  7070  infminti  7088  finomni  7201  nninfwlpoimlemginf  7237  isnumi  7244  oncardval  7248  archnqq  7479  prarloclemarch2  7481  prcdnql  7546  prcunqu  7547  prarloclemlo  7556  prarloclem5  7562  nqprm  7604  1idprl  7652  1idpru  7653  ltexpri  7675  prplnqu  7682  recexprlemm  7686  recexprlem1ssl  7695  recexprlem1ssu  7696  recexpr  7700  aptiprleml  7701  archpr  7705  cauappcvgprlemm  7707  cauappcvgprlemloc  7714  cauappcvgprlem1  7721  cauappcvgprlem2  7722  cauappcvgpr  7724  caucvgprlemm  7730  caucvgprlemloc  7737  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgprpr  7774  suplocexprlemmu  7780  suplocexprlemloc  7783  suplocexpr  7787  negexsr  7834  recexgt0sr  7835  caucvgsrlemgt1  7857  caucvgsrlemoffres  7862  suplocsrlem  7870  axrnegex  7941  axprecex  7942  nntopi  7956  axcaucvglemres  7961  axpre-suploclemres  7963  cnegex  8199  recexre  8599  recexap  8674  receuap  8690  rerecapb  8864  sup3exmid  8978  cju  8982  nn2ge  9017  nominpos  9223  zdiv  9408  btwnz  9439  supinfneg  9663  infsupneg  9664  ublbneg  9681  lbzbi  9684  zq  9694  z2ge  9895  iccsupr  10035  exbtwnzlemstep  10319  exbtwnzlemex  10321  rebtwn2zlemstep  10324  rebtwn2z  10326  qbtwnre  10328  qbtwnxr  10329  expnbnd  10737  hashunlem  10878  iswrdinn0  10922  shftlem  10963  shftfvalg  10965  shftfval  10968  caucvgre  11128  cvg1nlemres  11132  rexanuz  11135  rexuz3  11137  resqrexlemex  11172  caubnd2  11264  maxabslemval  11355  maxleast  11360  rexanre  11367  rexico  11368  fimaxre2  11373  minmax  11376  xrmaxiflemval  11396  xrmaxaddlem  11406  xrminmax  11411  climconst  11436  climshftlemg  11448  cn1lem  11460  serf0  11498  zsumdc  11530  fsum3  11533  fsum3cvg3  11542  mertenslemi1  11681  ntrivcvgap0  11695  zproddc  11725  fprodseq  11729  fprodntrivap  11730  dvdsval2  11936  dvds0lem  11947  dvds1lem  11948  dvds2lem  11949  odd2np1lem  12016  odd2np1  12017  opeo  12041  omeo  12042  divalglemex  12066  zsupcllemstep  12085  infssuzex  12089  suprzubdc  12092  zsupssdc  12094  bezoutlemnewy  12136  bezoutlemaz  12143  bezoutlembz  12144  bezoutlemsup  12149  nnwodc  12176  uzwodc  12177  ncoprmgcdne1b  12230  exprmfct  12279  reumodprminv  12394  modprm0  12395  nnnn0modprm0  12396  pythagtriplem19  12423  pcprmpw2  12474  pockthi  12499  infpnlem2  12501  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemrn  12579  ennnfonelemnn0  12582  ennnfonelemim  12584  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  ctiunctlemf  12598  ismgmid2  12966  mgmidsssn0  12970  ismndd  13021  isgrpd2  13096  isgrpd  13098  imasgrp2  13183  mhmmnd  13189  ghmgrp  13191  dvdsrmuld  13595  dvdsr01  13603  rhmdvdsr  13674  lspf  13888  lspval  13889  lssats2  13913  fiinbas  14228  topbas  14246  clsval  14290  neiint  14324  neipsm  14333  opnneissb  14334  opnssneib  14335  innei  14342  restbasg  14347  lmconst  14395  iscnp4  14397  cncnpi  14407  cnconst2  14412  cnptoprest  14418  cnpdis  14421  neitx  14447  txcnp  14450  blssps  14606  blss  14607  blssexps  14608  blssex  14609  ssblex  14610  blin2  14611  neibl  14670  metss2  14677  bdmopn  14683  metrest  14685  metcnp3  14690  tgioo  14733  tgqioo  14734  addcncntoplem  14740  cnopnap  14790  dedekindeulemuub  14796  suplociccreex  14803  dedekindicclemuub  14805  ivthinclemlm  14813  ivthinclemum  14814  ivthinclemlopn  14815  ivthinclemuopn  14817  ivthreinc  14824  elply2  14914  reeff1oleme  14948  sin0pilem2  14958  bj-nn0suc0  15512  bj-inf2vnlem1  15532  nninfsellemeq  15574  nninfomnilem  15578  qdencn  15587  trirec0  15604