Theorem rspcev 2868

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765

This theorem is referenced by:  rspceaimv  2876  rspc2ev  2883  rspc3ev  2885  rspceeqv  2886  reu6i  2955  rspesbca  3074  brralrspcev  4091  nn0suc  4640  elrnmpt1s  4916  elrnrexdm  5701  eldmrexrn  5703  foco2  5800  elabrex  5804  elabrexg  5805  f1elima  5820  fcofo  5831  fliftfun  5843  fliftval  5847  f1oiso2  5874  fo1st  6215  fo2nd  6216  tfr0dm  6380  tfrlemisucaccv  6383  tfrlemi14d  6391  tfrexlem  6392  tfr1onlemsucaccv  6399  tfr1onlemres  6407  tfrcllemsucaccv  6412  tfrcllemres  6420  rdgss  6441  frecabcl  6457  nnaordex  6586  nnawordex  6587  ecelqsg  6647  snfig  6873  nnfi  6933  findcard  6949  fimax2gtrilemstep  6961  unsnfi  6980  eqsupti  7062  supmaxti  7070  supisoex  7075  infminti  7093  finomni  7206  nninfwlpoimlemginf  7242  isnumi  7249  oncardval  7253  archnqq  7484  prarloclemarch2  7486  prcdnql  7551  prcunqu  7552  prarloclemlo  7561  prarloclem5  7567  nqprm  7609  1idprl  7657  1idpru  7658  ltexpri  7680  prplnqu  7687  recexprlemm  7691  recexprlem1ssl  7700  recexprlem1ssu  7701  recexpr  7705  aptiprleml  7706  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemloc  7719  cauappcvgprlem1  7726  cauappcvgprlem2  7727  cauappcvgpr  7729  caucvgprlemm  7735  caucvgprlemloc  7742  caucvgprlem1  7746  caucvgprlem2  7747  caucvgpr  7749  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgprpr  7779  suplocexprlemmu  7785  suplocexprlemloc  7788  suplocexpr  7792  negexsr  7839  recexgt0sr  7840  caucvgsrlemgt1  7862  caucvgsrlemoffres  7867  suplocsrlem  7875  axrnegex  7946  axprecex  7947  nntopi  7961  axcaucvglemres  7966  axpre-suploclemres  7968  cnegex  8204  recexre  8605  recexap  8680  receuap  8696  rerecapb  8870  sup3exmid  8984  cju  8988  nn2ge  9023  nominpos  9229  zdiv  9414  btwnz  9445  supinfneg  9669  infsupneg  9670  ublbneg  9687  lbzbi  9690  zq  9700  z2ge  9901  iccsupr  10041  zsupcllemstep  10319  infssuzex  10323  suprzubdc  10326  zsupssdc  10328  exbtwnzlemstep  10337  exbtwnzlemex  10339  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnre  10346  qbtwnxr  10347  expnbnd  10755  hashunlem  10896  iswrdinn0  10940  shftlem  10981  shftfvalg  10983  shftfval  10986  caucvgre  11146  cvg1nlemres  11150  rexanuz  11153  rexuz3  11155  resqrexlemex  11190  caubnd2  11282  maxabslemval  11373  maxleast  11378  rexanre  11385  rexico  11386  fimaxre2  11392  minmax  11395  xrmaxiflemval  11415  xrmaxaddlem  11425  xrminmax  11430  climconst  11455  climshftlemg  11467  cn1lem  11479  serf0  11517  zsumdc  11549  fsum3  11552  fsum3cvg3  11561  mertenslemi1  11700  ntrivcvgap0  11714  zproddc  11744  fprodseq  11748  fprodntrivap  11749  dvdsval2  11955  dvds0lem  11966  dvds1lem  11967  dvds2lem  11968  odd2np1lem  12037  odd2np1  12038  opeo  12062  omeo  12063  divalglemex  12087  bezoutlemnewy  12163  bezoutlemaz  12170  bezoutlembz  12171  bezoutlemsup  12176  nnwodc  12203  uzwodc  12204  ncoprmgcdne1b  12257  exprmfct  12306  reumodprminv  12422  modprm0  12423  nnnn0modprm0  12424  pythagtriplem19  12451  pcprmpw2  12502  pockthi  12527  infpnlem2  12529  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemrn  12636  ennnfonelemnn0  12639  ennnfonelemim  12641  exmidunben  12643  ctinfomlemom  12644  ctinfom  12645  ctinf  12647  ctiunctlemf  12655  ismgmid2  13023  mgmidsssn0  13027  ismndd  13078  isgrpd2  13153  isgrpd  13155  imasgrp2  13240  mhmmnd  13246  ghmgrp  13248  dvdsrmuld  13652  dvdsr01  13660  rhmdvdsr  13731  lspf  13945  lspval  13946  lssats2  13970  fiinbas  14285  topbas  14303  clsval  14347  neiint  14381  neipsm  14390  opnneissb  14391  opnssneib  14392  innei  14399  restbasg  14404  lmconst  14452  iscnp4  14454  cncnpi  14464  cnconst2  14469  cnptoprest  14475  cnpdis  14478  neitx  14504  txcnp  14507  blssps  14663  blss  14664  blssexps  14665  blssex  14666  ssblex  14667  blin2  14668  neibl  14727  metss2  14734  bdmopn  14740  metrest  14742  metcnp3  14747  tgioo  14790  tgqioo  14791  addcncntoplem  14797  cnopnap  14847  dedekindeulemuub  14853  suplociccreex  14860  dedekindicclemuub  14862  ivthinclemlm  14870  ivthinclemum  14871  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthreinc  14881  elply2  14971  reeff1oleme  15008  sin0pilem2  15018  sgmnncl  15224  dvdsppwf1o  15225  perfect  15237  bj-nn0suc0  15596  bj-inf2vnlem1  15616  nninfsellemeq  15658  nninfomnilem  15662  qdencn  15671  trirec0  15688