Theorem rspcev 2929

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823

This theorem is used by:  rspcedvdw  2936  rspceaimv  2938  rspc2ev  2945  rspc3ev  2947  rspceeqv  2948  reu6i  3017  rspesbca  3137  brralrspcev  4189  nn0suc  4751  elrnmpt1s  5032  elrnrexdm  5847  eldmrexrn  5849  foco2  5959  elabrex  5963  elabrexg  5964  f1elima  5979  fcofo  5990  fliftfun  6002  fliftval  6006  f1oiso2  6033  fo1st  6391  fo2nd  6392  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllemres  6633  rdgss  6654  frecabcl  6670  nnaordex  6801  nnawordex  6802  ecelqsg  6862  snfig  7103  nnfi  7174  findcard  7192  fimax2gtrilemstep  7205  unsnfi  7226  eqsupti  7336  supmaxti  7344  supisoex  7349  infminti  7367  finomni  7480  nninfwlpoimlemginf  7516  isnumi  7527  oncardval  7531  archnqq  7784  prarloclemarch2  7786  prcdnql  7851  prcunqu  7852  prarloclemlo  7861  prarloclem5  7867  nqprm  7909  1idprl  7957  1idpru  7958  ltexpri  7980  prplnqu  7987  recexprlemm  7991  recexprlem1ssl  8000  recexprlem1ssu  8001  recexpr  8005  aptiprleml  8006  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  cauappcvgpr  8029  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlem1  8046  caucvgprlem2  8047  caucvgpr  8049  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgprpr  8079  suplocexprlemmu  8085  suplocexprlemloc  8088  suplocexpr  8092  negexsr  8139  recexgt0sr  8140  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  suplocsrlem  8175  axrnegex  8246  axprecex  8247  nntopi  8261  axcaucvglemres  8266  axpre-suploclemres  8268  cnegex  8504  recexre  8906  recexap  8981  receuap  8999  rerecapb  9173  sup3exmid  9287  cju  9291  nn2ge  9337  nominpos  9543  zdiv  9734  btwnz  9765  supinfneg  9995  infsupneg  9996  ublbneg  10013  lbzbi  10016  zq  10026  z2ge  10228  iccsupr  10368  zsupcllemstep  10662  infssuzex  10666  suprzubdc  10671  zsupssdc  10673  exbtwnzlemstep  10682  exbtwnzlemex  10684  rebtwn2zlemstep  10687  rebtwn2z  10689  qbtwnre  10691  qbtwnxr  10692  expnbnd  11101  hashunlem  11244  iswrdinn0  11309  shftlem  11581  shftfvalg  11583  shftfval  11586  caucvgre  11747  cvg1nlemres  11751  rexanuz  11754  rexuz3  11756  resqrexlemex  11791  caubnd2  11883  maxabslemval  11974  maxleast  11979  rexanre  11986  rexico  11987  fimaxre2  11993  minmax  11996  xrmaxiflemval  12016  xrmaxaddlem  12026  xrminmax  12031  climconst  12056  climshftlemg  12068  cn1lem  12080  serf0  12118  zsumdc  12151  fsum3  12154  fsum3cvg3  12163  mertenslemi1  12302  ntrivcvgap0  12316  zproddc  12346  fprodseq  12350  fprodntrivap  12351  dvdsval2  12557  dvds0lem  12568  dvds1lem  12569  dvds2lem  12570  odd2np1lem  12639  odd2np1  12640  opeo  12664  omeo  12665  divalglemex  12689  bezoutlemnewy  12773  bezoutlemaz  12780  bezoutlembz  12781  bezoutlemsup  12786  nnwodc  12813  uzwodc  12814  ncoprmgcdne1b  12867  exprmfct  12916  reumodprminv  13032  modprm0  13033  nnnn0modprm0  13034  pythagtriplem19  13061  pcprmpw2  13112  pockthi  13137  infpnlem2  13139  ballotfilem4  13241  ballotfilemic  13250  ennnfonelemex  13305  ennnfonelemhom  13306  ennnfonelemrn  13310  ennnfonelemnn0  13313  ennnfonelemim  13315  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  ctiunctlemf  13329  ismgmid2  13700  mgmidsssn0  13704  ismndd  13750  isgrpd2  13826  isgrpd  13828  imasgrp2  13913  mhmmnd  13919  ghmgrp  13921  dvdsrmuld  14403  dvdsr01  14411  rhmdvdsr  14482  lspf  14726  lspval  14727  lssats2  14751  aspval  15015  fiinbas  15150  topbas  15168  clsval  15212  neiint  15246  neipsm  15255  opnneissb  15256  opnssneib  15257  innei  15264  restbasg  15269  lmconst  15317  iscnp4  15319  cncnpi  15329  cnconst2  15334  cnptoprest  15340  cnpdis  15343  neitx  15369  txcnp  15372  blssps  15528  blss  15529  blssexps  15530  blssex  15531  ssblex  15532  blin2  15533  neibl  15592  metss2  15599  bdmopn  15605  metrest  15607  metcnp3  15612  tgioo  15655  tgqioo  15656  addcncntoplem  15662  cnopnap  15712  dedekindeulemuub  15718  suplociccreex  15725  dedekindicclemuub  15727  ivthinclemlm  15735  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthreinc  15746  elply2  15836  reeff1oleme  15873  sin0pilem2  15883  sgmnncl  16102  dvdsppwf1o  16103  perfect  16115  bj-nn0suc0  16976  bj-inf2vnlem1  16996  3dom  17018  nninfsellemeq  17057  nninfomnilem  17061  qdencn  17072  trirec0  17093  qdiff  17098