Theorem rspcev 2842

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   E.wrex 2456

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740

This theorem is referenced by:  rspceaimv  2850  rspc2ev  2857  rspc3ev  2859  rspceeqv  2860  reu6i  2929  rspesbca  3048  brralrspcev  4062  nn0suc  4604  elrnmpt1s  4878  elrnrexdm  5656  eldmrexrn  5658  foco2  5755  elabrex  5759  f1elima  5774  fcofo  5785  fliftfun  5797  fliftval  5801  f1oiso2  5828  fo1st  6158  fo2nd  6159  tfr0dm  6323  tfrlemisucaccv  6326  tfrlemi14d  6334  tfrexlem  6335  tfr1onlemsucaccv  6342  tfr1onlemres  6350  tfrcllemsucaccv  6355  tfrcllemres  6363  rdgss  6384  frecabcl  6400  nnaordex  6529  nnawordex  6530  ecelqsg  6588  snfig  6814  nnfi  6872  findcard  6888  fimax2gtrilemstep  6900  unsnfi  6918  eqsupti  6995  supmaxti  7003  supisoex  7008  infminti  7026  finomni  7138  nninfwlpoimlemginf  7174  isnumi  7181  oncardval  7185  archnqq  7416  prarloclemarch2  7418  prcdnql  7483  prcunqu  7484  prarloclemlo  7493  prarloclem5  7499  nqprm  7541  1idprl  7589  1idpru  7590  ltexpri  7612  prplnqu  7619  recexprlemm  7623  recexprlem1ssl  7632  recexprlem1ssu  7633  recexpr  7637  aptiprleml  7638  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemloc  7651  cauappcvgprlem1  7658  cauappcvgprlem2  7659  cauappcvgpr  7661  caucvgprlemm  7667  caucvgprlemloc  7674  caucvgprlem1  7678  caucvgprlem2  7679  caucvgpr  7681  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgprpr  7711  suplocexprlemmu  7717  suplocexprlemloc  7720  suplocexpr  7724  negexsr  7771  recexgt0sr  7772  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  suplocsrlem  7807  axrnegex  7878  axprecex  7879  nntopi  7893  axcaucvglemres  7898  axpre-suploclemres  7900  cnegex  8135  recexre  8535  recexap  8610  receuap  8626  rerecapb  8800  sup3exmid  8914  cju  8918  nn2ge  8952  nominpos  9156  zdiv  9341  btwnz  9372  supinfneg  9595  infsupneg  9596  ublbneg  9613  lbzbi  9616  zq  9626  z2ge  9826  iccsupr  9966  exbtwnzlemstep  10248  exbtwnzlemex  10250  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnre  10257  qbtwnxr  10258  expnbnd  10644  hashunlem  10784  shftlem  10825  shftfvalg  10827  shftfval  10830  caucvgre  10990  cvg1nlemres  10994  rexanuz  10997  rexuz3  10999  resqrexlemex  11034  caubnd2  11126  maxabslemval  11217  maxleast  11222  rexanre  11229  rexico  11230  fimaxre2  11235  minmax  11238  xrmaxiflemval  11258  xrmaxaddlem  11268  xrminmax  11273  climconst  11298  climshftlemg  11310  cn1lem  11322  serf0  11360  zsumdc  11392  fsum3  11395  fsum3cvg3  11404  mertenslemi1  11543  ntrivcvgap0  11557  zproddc  11587  fprodseq  11591  fprodntrivap  11592  dvdsval2  11797  dvds0lem  11808  dvds1lem  11809  dvds2lem  11810  odd2np1lem  11877  odd2np1  11878  opeo  11902  omeo  11903  divalglemex  11927  zsupcllemstep  11946  infssuzex  11950  suprzubdc  11953  zsupssdc  11955  bezoutlemnewy  11997  bezoutlemaz  12004  bezoutlembz  12005  bezoutlemsup  12010  nnwodc  12037  uzwodc  12038  ncoprmgcdne1b  12089  exprmfct  12138  reumodprminv  12253  modprm0  12254  nnnn0modprm0  12255  pythagtriplem19  12282  pcprmpw2  12332  pockthi  12356  infpnlem2  12358  ennnfonelemex  12415  ennnfonelemhom  12416  ennnfonelemrn  12420  ennnfonelemnn0  12423  ennnfonelemim  12425  exmidunben  12427  ctinfomlemom  12428  ctinfom  12429  ctinf  12431  ctiunctlemf  12439  ismgmid2  12799  mgmidsssn0  12803  ismndd  12838  isgrpd2  12897  isgrpd  12899  mhmmnd  12980  ghmgrp  12982  dvdsrmuld  13265  dvdsr01  13273  fiinbas  13552  topbas  13570  clsval  13614  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  innei  13666  restbasg  13671  lmconst  13719  iscnp4  13721  cncnpi  13731  cnconst2  13736  cnptoprest  13742  cnpdis  13745  neitx  13771  txcnp  13774  blssps  13930  blss  13931  blssexps  13932  blssex  13933  ssblex  13934  blin2  13935  neibl  13994  metss2  14001  bdmopn  14007  metrest  14009  metcnp3  14014  tgioo  14049  tgqioo  14050  addcncntoplem  14054  cnopnap  14097  dedekindeulemuub  14098  suplociccreex  14105  dedekindicclemuub  14107  ivthinclemlm  14115  ivthinclemum  14116  ivthinclemlopn  14117  ivthinclemuopn  14119  reeff1oleme  14196  sin0pilem2  14206  bj-nn0suc0  14705  bj-inf2vnlem1  14725  nninfsellemeq  14766  nninfomnilem  14770  qdencn  14778  trirec0  14795