Theorem rspcev 2907

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   E.wrex 2509

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801

This theorem is referenced by:  rspceaimv  2915  rspc2ev  2922  rspc3ev  2924  rspceeqv  2925  reu6i  2994  rspesbca  3114  brralrspcev  4142  nn0suc  4696  elrnmpt1s  4974  elrnrexdm  5776  eldmrexrn  5778  foco2  5883  elabrex  5887  elabrexg  5888  f1elima  5903  fcofo  5914  fliftfun  5926  fliftval  5930  f1oiso2  5957  fo1st  6309  fo2nd  6310  tfr0dm  6474  tfrlemisucaccv  6477  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemsucaccv  6493  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllemres  6514  rdgss  6535  frecabcl  6551  nnaordex  6682  nnawordex  6683  ecelqsg  6743  snfig  6975  nnfi  7042  findcard  7058  fimax2gtrilemstep  7071  unsnfi  7092  eqsupti  7174  supmaxti  7182  supisoex  7187  infminti  7205  finomni  7318  nninfwlpoimlemginf  7354  isnumi  7365  oncardval  7369  archnqq  7615  prarloclemarch2  7617  prcdnql  7682  prcunqu  7683  prarloclemlo  7692  prarloclem5  7698  nqprm  7740  1idprl  7788  1idpru  7789  ltexpri  7811  prplnqu  7818  recexprlemm  7822  recexprlem1ssl  7831  recexprlem1ssu  7832  recexpr  7836  aptiprleml  7837  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemloc  7850  cauappcvgprlem1  7857  cauappcvgprlem2  7858  cauappcvgpr  7860  caucvgprlemm  7866  caucvgprlemloc  7873  caucvgprlem1  7877  caucvgprlem2  7878  caucvgpr  7880  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgprpr  7910  suplocexprlemmu  7916  suplocexprlemloc  7919  suplocexpr  7923  negexsr  7970  recexgt0sr  7971  caucvgsrlemgt1  7993  caucvgsrlemoffres  7998  suplocsrlem  8006  axrnegex  8077  axprecex  8078  nntopi  8092  axcaucvglemres  8097  axpre-suploclemres  8099  cnegex  8335  recexre  8736  recexap  8811  receuap  8827  rerecapb  9001  sup3exmid  9115  cju  9119  nn2ge  9154  nominpos  9360  zdiv  9546  btwnz  9577  supinfneg  9802  infsupneg  9803  ublbneg  9820  lbzbi  9823  zq  9833  z2ge  10034  iccsupr  10174  zsupcllemstep  10461  infssuzex  10465  suprzubdc  10468  zsupssdc  10470  exbtwnzlemstep  10479  exbtwnzlemex  10481  rebtwn2zlemstep  10484  rebtwn2z  10486  qbtwnre  10488  qbtwnxr  10489  expnbnd  10897  hashunlem  11038  iswrdinn0  11089  shftlem  11343  shftfvalg  11345  shftfval  11348  caucvgre  11508  cvg1nlemres  11512  rexanuz  11515  rexuz3  11517  resqrexlemex  11552  caubnd2  11644  maxabslemval  11735  maxleast  11740  rexanre  11747  rexico  11748  fimaxre2  11754  minmax  11757  xrmaxiflemval  11777  xrmaxaddlem  11787  xrminmax  11792  climconst  11817  climshftlemg  11829  cn1lem  11841  serf0  11879  zsumdc  11911  fsum3  11914  fsum3cvg3  11923  mertenslemi1  12062  ntrivcvgap0  12076  zproddc  12106  fprodseq  12110  fprodntrivap  12111  dvdsval2  12317  dvds0lem  12328  dvds1lem  12329  dvds2lem  12330  odd2np1lem  12399  odd2np1  12400  opeo  12424  omeo  12425  divalglemex  12449  bezoutlemnewy  12533  bezoutlemaz  12540  bezoutlembz  12541  bezoutlemsup  12546  nnwodc  12573  uzwodc  12574  ncoprmgcdne1b  12627  exprmfct  12676  reumodprminv  12792  modprm0  12793  nnnn0modprm0  12794  pythagtriplem19  12821  pcprmpw2  12872  pockthi  12897  infpnlem2  12899  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemrn  13006  ennnfonelemnn0  13009  ennnfonelemim  13011  exmidunben  13013  ctinfomlemom  13014  ctinfom  13015  ctinf  13017  ctiunctlemf  13025  ismgmid2  13429  mgmidsssn0  13433  ismndd  13486  isgrpd2  13570  isgrpd  13572  imasgrp2  13663  mhmmnd  13669  ghmgrp  13671  dvdsrmuld  14076  dvdsr01  14084  rhmdvdsr  14155  lspf  14369  lspval  14370  lssats2  14394  fiinbas  14739  topbas  14757  clsval  14801  neiint  14835  neipsm  14844  opnneissb  14845  opnssneib  14846  innei  14853  restbasg  14858  lmconst  14906  iscnp4  14908  cncnpi  14918  cnconst2  14923  cnptoprest  14929  cnpdis  14932  neitx  14958  txcnp  14961  blssps  15117  blss  15118  blssexps  15119  blssex  15120  ssblex  15121  blin2  15122  neibl  15181  metss2  15188  bdmopn  15194  metrest  15196  metcnp3  15201  tgioo  15244  tgqioo  15245  addcncntoplem  15251  cnopnap  15301  dedekindeulemuub  15307  suplociccreex  15314  dedekindicclemuub  15316  ivthinclemlm  15324  ivthinclemum  15325  ivthinclemlopn  15326  ivthinclemuopn  15328  ivthreinc  15335  elply2  15425  reeff1oleme  15462  sin0pilem2  15472  sgmnncl  15678  dvdsppwf1o  15679  perfect  15691  bj-nn0suc0  16396  bj-inf2vnlem1  16416  3dom  16439  nninfsellemeq  16468  nninfomnilem  16472  qdencn  16483  trirec0  16500