Theorem rspcev 2864

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 2859	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  2872  rspc2ev  2879  rspc3ev  2881  rspceeqv  2882  reu6i  2951  rspesbca  3070  brralrspcev  4087  nn0suc  4636  elrnmpt1s  4912  elrnrexdm  5697  eldmrexrn  5699  foco2  5796  elabrex  5800  elabrexg  5801  f1elima  5816  fcofo  5827  fliftfun  5839  fliftval  5843  f1oiso2  5870  fo1st  6210  fo2nd  6211  tfr0dm  6375  tfrlemisucaccv  6378  tfrlemi14d  6386  tfrexlem  6387  tfr1onlemsucaccv  6394  tfr1onlemres  6402  tfrcllemsucaccv  6407  tfrcllemres  6415  rdgss  6436  frecabcl  6452  nnaordex  6581  nnawordex  6582  ecelqsg  6642  snfig  6868  nnfi  6928  findcard  6944  fimax2gtrilemstep  6956  unsnfi  6975  eqsupti  7055  supmaxti  7063  supisoex  7068  infminti  7086  finomni  7199  nninfwlpoimlemginf  7235  isnumi  7242  oncardval  7246  archnqq  7477  prarloclemarch2  7479  prcdnql  7544  prcunqu  7545  prarloclemlo  7554  prarloclem5  7560  nqprm  7602  1idprl  7650  1idpru  7651  ltexpri  7673  prplnqu  7680  recexprlemm  7684  recexprlem1ssl  7693  recexprlem1ssu  7694  recexpr  7698  aptiprleml  7699  archpr  7703  cauappcvgprlemm  7705  cauappcvgprlemloc  7712  cauappcvgprlem1  7719  cauappcvgprlem2  7720  cauappcvgpr  7722  caucvgprlemm  7728  caucvgprlemloc  7735  caucvgprlem1  7739  caucvgprlem2  7740  caucvgpr  7742  caucvgprprlemmu  7755  caucvgprprlemopl  7757  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlem1  7769  caucvgprprlem2  7770  caucvgprpr  7772  suplocexprlemmu  7778  suplocexprlemloc  7781  suplocexpr  7785  negexsr  7832  recexgt0sr  7833  caucvgsrlemgt1  7855  caucvgsrlemoffres  7860  suplocsrlem  7868  axrnegex  7939  axprecex  7940  nntopi  7954  axcaucvglemres  7959  axpre-suploclemres  7961  cnegex  8197  recexre  8597  recexap  8672  receuap  8688  rerecapb  8862  sup3exmid  8976  cju  8980  nn2ge  9015  nominpos  9220  zdiv  9405  btwnz  9436  supinfneg  9660  infsupneg  9661  ublbneg  9678  lbzbi  9681  zq  9691  z2ge  9892  iccsupr  10032  exbtwnzlemstep  10316  exbtwnzlemex  10318  rebtwn2zlemstep  10321  rebtwn2z  10323  qbtwnre  10325  qbtwnxr  10326  expnbnd  10734  hashunlem  10875  iswrdinn0  10919  shftlem  10960  shftfvalg  10962  shftfval  10965  caucvgre  11125  cvg1nlemres  11129  rexanuz  11132  rexuz3  11134  resqrexlemex  11169  caubnd2  11261  maxabslemval  11352  maxleast  11357  rexanre  11364  rexico  11365  fimaxre2  11370  minmax  11373  xrmaxiflemval  11393  xrmaxaddlem  11403  xrminmax  11408  climconst  11433  climshftlemg  11445  cn1lem  11457  serf0  11495  zsumdc  11527  fsum3  11530  fsum3cvg3  11539  mertenslemi1  11678  ntrivcvgap0  11692  zproddc  11722  fprodseq  11726  fprodntrivap  11727  dvdsval2  11933  dvds0lem  11944  dvds1lem  11945  dvds2lem  11946  odd2np1lem  12013  odd2np1  12014  opeo  12038  omeo  12039  divalglemex  12063  zsupcllemstep  12082  infssuzex  12086  suprzubdc  12089  zsupssdc  12091  bezoutlemnewy  12133  bezoutlemaz  12140  bezoutlembz  12141  bezoutlemsup  12146  nnwodc  12173  uzwodc  12174  ncoprmgcdne1b  12227  exprmfct  12276  reumodprminv  12391  modprm0  12392  nnnn0modprm0  12393  pythagtriplem19  12420  pcprmpw2  12471  pockthi  12496  infpnlem2  12498  ennnfonelemex  12571  ennnfonelemhom  12572  ennnfonelemrn  12576  ennnfonelemnn0  12579  ennnfonelemim  12581  exmidunben  12583  ctinfomlemom  12584  ctinfom  12585  ctinf  12587  ctiunctlemf  12595  ismgmid2  12963  mgmidsssn0  12967  ismndd  13018  isgrpd2  13093  isgrpd  13095  imasgrp2  13180  mhmmnd  13186  ghmgrp  13188  dvdsrmuld  13592  dvdsr01  13600  rhmdvdsr  13671  lspf  13885  lspval  13886  lssats2  13910  fiinbas  14217  topbas  14235  clsval  14279  neiint  14313  neipsm  14322  opnneissb  14323  opnssneib  14324  innei  14331  restbasg  14336  lmconst  14384  iscnp4  14386  cncnpi  14396  cnconst2  14401  cnptoprest  14407  cnpdis  14410  neitx  14436  txcnp  14439  blssps  14595  blss  14596  blssexps  14597  blssex  14598  ssblex  14599  blin2  14600  neibl  14659  metss2  14666  bdmopn  14672  metrest  14674  metcnp3  14679  tgioo  14714  tgqioo  14715  addcncntoplem  14719  cnopnap  14765  dedekindeulemuub  14771  suplociccreex  14778  dedekindicclemuub  14780  ivthinclemlm  14788  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthreinc  14799  elply2  14881  reeff1oleme  14907  sin0pilem2  14917  bj-nn0suc0  15442  bj-inf2vnlem1  15462  nninfsellemeq  15504  nninfomnilem  15508  qdencn  15517  trirec0  15534