Theorem rspcev 2843

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 2838	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 2741

This theorem is referenced by:  rspceaimv  2851  rspc2ev  2858  rspc3ev  2860  rspceeqv  2861  reu6i  2930  rspesbca  3049  brralrspcev  4063  nn0suc  4605  elrnmpt1s  4879  elrnrexdm  5658  eldmrexrn  5660  foco2  5757  elabrex  5761  elabrexg  5762  f1elima  5777  fcofo  5788  fliftfun  5800  fliftval  5804  f1oiso2  5831  fo1st  6161  fo2nd  6162  tfr0dm  6326  tfrlemisucaccv  6329  tfrlemi14d  6337  tfrexlem  6338  tfr1onlemsucaccv  6345  tfr1onlemres  6353  tfrcllemsucaccv  6358  tfrcllemres  6366  rdgss  6387  frecabcl  6403  nnaordex  6532  nnawordex  6533  ecelqsg  6591  snfig  6817  nnfi  6875  findcard  6891  fimax2gtrilemstep  6903  unsnfi  6921  eqsupti  6998  supmaxti  7006  supisoex  7011  infminti  7029  finomni  7141  nninfwlpoimlemginf  7177  isnumi  7184  oncardval  7188  archnqq  7419  prarloclemarch2  7421  prcdnql  7486  prcunqu  7487  prarloclemlo  7496  prarloclem5  7502  nqprm  7544  1idprl  7592  1idpru  7593  ltexpri  7615  prplnqu  7622  recexprlemm  7626  recexprlem1ssl  7635  recexprlem1ssu  7636  recexpr  7640  aptiprleml  7641  archpr  7645  cauappcvgprlemm  7647  cauappcvgprlemloc  7654  cauappcvgprlem1  7661  cauappcvgprlem2  7662  cauappcvgpr  7664  caucvgprlemm  7670  caucvgprlemloc  7677  caucvgprlem1  7681  caucvgprlem2  7682  caucvgpr  7684  caucvgprprlemmu  7697  caucvgprprlemopl  7699  caucvgprprlemopu  7701  caucvgprprlemloc  7705  caucvgprprlem1  7711  caucvgprprlem2  7712  caucvgprpr  7714  suplocexprlemmu  7720  suplocexprlemloc  7723  suplocexpr  7727  negexsr  7774  recexgt0sr  7775  caucvgsrlemgt1  7797  caucvgsrlemoffres  7802  suplocsrlem  7810  axrnegex  7881  axprecex  7882  nntopi  7896  axcaucvglemres  7901  axpre-suploclemres  7903  cnegex  8138  recexre  8538  recexap  8613  receuap  8629  rerecapb  8803  sup3exmid  8917  cju  8921  nn2ge  8955  nominpos  9159  zdiv  9344  btwnz  9375  supinfneg  9598  infsupneg  9599  ublbneg  9616  lbzbi  9619  zq  9629  z2ge  9829  iccsupr  9969  exbtwnzlemstep  10251  exbtwnzlemex  10253  rebtwn2zlemstep  10256  rebtwn2z  10258  qbtwnre  10260  qbtwnxr  10261  expnbnd  10647  hashunlem  10787  shftlem  10828  shftfvalg  10830  shftfval  10833  caucvgre  10993  cvg1nlemres  10997  rexanuz  11000  rexuz3  11002  resqrexlemex  11037  caubnd2  11129  maxabslemval  11220  maxleast  11225  rexanre  11232  rexico  11233  fimaxre2  11238  minmax  11241  xrmaxiflemval  11261  xrmaxaddlem  11271  xrminmax  11276  climconst  11301  climshftlemg  11313  cn1lem  11325  serf0  11363  zsumdc  11395  fsum3  11398  fsum3cvg3  11407  mertenslemi1  11546  ntrivcvgap0  11560  zproddc  11590  fprodseq  11594  fprodntrivap  11595  dvdsval2  11800  dvds0lem  11811  dvds1lem  11812  dvds2lem  11813  odd2np1lem  11880  odd2np1  11881  opeo  11905  omeo  11906  divalglemex  11930  zsupcllemstep  11949  infssuzex  11953  suprzubdc  11956  zsupssdc  11958  bezoutlemnewy  12000  bezoutlemaz  12007  bezoutlembz  12008  bezoutlemsup  12013  nnwodc  12040  uzwodc  12041  ncoprmgcdne1b  12092  exprmfct  12141  reumodprminv  12256  modprm0  12257  nnnn0modprm0  12258  pythagtriplem19  12285  pcprmpw2  12335  pockthi  12359  infpnlem2  12361  ennnfonelemex  12418  ennnfonelemhom  12419  ennnfonelemrn  12423  ennnfonelemnn0  12426  ennnfonelemim  12428  exmidunben  12430  ctinfomlemom  12431  ctinfom  12432  ctinf  12434  ctiunctlemf  12442  ismgmid2  12806  mgmidsssn0  12810  ismndd  12846  isgrpd2  12905  isgrpd  12907  imasgrp2  12989  mhmmnd  12993  ghmgrp  12995  dvdsrmuld  13303  dvdsr01  13311  lspf  13514  lspval  13515  lssats2  13539  fiinbas  13737  topbas  13755  clsval  13799  neiint  13833  neipsm  13842  opnneissb  13843  opnssneib  13844  innei  13851  restbasg  13856  lmconst  13904  iscnp4  13906  cncnpi  13916  cnconst2  13921  cnptoprest  13927  cnpdis  13930  neitx  13956  txcnp  13959  blssps  14115  blss  14116  blssexps  14117  blssex  14118  ssblex  14119  blin2  14120  neibl  14179  metss2  14186  bdmopn  14192  metrest  14194  metcnp3  14199  tgioo  14234  tgqioo  14235  addcncntoplem  14239  cnopnap  14282  dedekindeulemuub  14283  suplociccreex  14290  dedekindicclemuub  14292  ivthinclemlm  14300  ivthinclemum  14301  ivthinclemlopn  14302  ivthinclemuopn  14304  reeff1oleme  14381  sin0pilem2  14391  bj-nn0suc0  14890  bj-inf2vnlem1  14910  nninfsellemeq  14952  nninfomnilem  14956  qdencn  14964  trirec0  14981