Theorem rspcev 2884

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   e. wcel 2178   E.wrex 2487

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778

This theorem is referenced by:  rspceaimv  2892  rspc2ev  2899  rspc3ev  2901  rspceeqv  2902  reu6i  2971  rspesbca  3091  brralrspcev  4118  nn0suc  4670  elrnmpt1s  4947  elrnrexdm  5742  eldmrexrn  5744  foco2  5845  elabrex  5849  elabrexg  5850  f1elima  5865  fcofo  5876  fliftfun  5888  fliftval  5892  f1oiso2  5919  fo1st  6266  fo2nd  6267  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemi14d  6442  tfrexlem  6443  tfr1onlemsucaccv  6450  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllemres  6471  rdgss  6492  frecabcl  6508  nnaordex  6637  nnawordex  6638  ecelqsg  6698  snfig  6930  nnfi  6995  findcard  7011  fimax2gtrilemstep  7023  unsnfi  7042  eqsupti  7124  supmaxti  7132  supisoex  7137  infminti  7155  finomni  7268  nninfwlpoimlemginf  7304  isnumi  7315  oncardval  7319  archnqq  7565  prarloclemarch2  7567  prcdnql  7632  prcunqu  7633  prarloclemlo  7642  prarloclem5  7648  nqprm  7690  1idprl  7738  1idpru  7739  ltexpri  7761  prplnqu  7768  recexprlemm  7772  recexprlem1ssl  7781  recexprlem1ssu  7782  recexpr  7786  aptiprleml  7787  archpr  7791  cauappcvgprlemm  7793  cauappcvgprlemloc  7800  cauappcvgprlem1  7807  cauappcvgprlem2  7808  cauappcvgpr  7810  caucvgprlemm  7816  caucvgprlemloc  7823  caucvgprlem1  7827  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgprpr  7860  suplocexprlemmu  7866  suplocexprlemloc  7869  suplocexpr  7873  negexsr  7920  recexgt0sr  7921  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  suplocsrlem  7956  axrnegex  8027  axprecex  8028  nntopi  8042  axcaucvglemres  8047  axpre-suploclemres  8049  cnegex  8285  recexre  8686  recexap  8761  receuap  8777  rerecapb  8951  sup3exmid  9065  cju  9069  nn2ge  9104  nominpos  9310  zdiv  9496  btwnz  9527  supinfneg  9751  infsupneg  9752  ublbneg  9769  lbzbi  9772  zq  9782  z2ge  9983  iccsupr  10123  zsupcllemstep  10409  infssuzex  10413  suprzubdc  10416  zsupssdc  10418  exbtwnzlemstep  10427  exbtwnzlemex  10429  rebtwn2zlemstep  10432  rebtwn2z  10434  qbtwnre  10436  qbtwnxr  10437  expnbnd  10845  hashunlem  10986  iswrdinn0  11036  shftlem  11242  shftfvalg  11244  shftfval  11247  caucvgre  11407  cvg1nlemres  11411  rexanuz  11414  rexuz3  11416  resqrexlemex  11451  caubnd2  11543  maxabslemval  11634  maxleast  11639  rexanre  11646  rexico  11647  fimaxre2  11653  minmax  11656  xrmaxiflemval  11676  xrmaxaddlem  11686  xrminmax  11691  climconst  11716  climshftlemg  11728  cn1lem  11740  serf0  11778  zsumdc  11810  fsum3  11813  fsum3cvg3  11822  mertenslemi1  11961  ntrivcvgap0  11975  zproddc  12005  fprodseq  12009  fprodntrivap  12010  dvdsval2  12216  dvds0lem  12227  dvds1lem  12228  dvds2lem  12229  odd2np1lem  12298  odd2np1  12299  opeo  12323  omeo  12324  divalglemex  12348  bezoutlemnewy  12432  bezoutlemaz  12439  bezoutlembz  12440  bezoutlemsup  12445  nnwodc  12472  uzwodc  12473  ncoprmgcdne1b  12526  exprmfct  12575  reumodprminv  12691  modprm0  12692  nnnn0modprm0  12693  pythagtriplem19  12720  pcprmpw2  12771  pockthi  12796  infpnlem2  12798  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemrn  12905  ennnfonelemnn0  12908  ennnfonelemim  12910  exmidunben  12912  ctinfomlemom  12913  ctinfom  12914  ctinf  12916  ctiunctlemf  12924  ismgmid2  13327  mgmidsssn0  13331  ismndd  13384  isgrpd2  13468  isgrpd  13470  imasgrp2  13561  mhmmnd  13567  ghmgrp  13569  dvdsrmuld  13973  dvdsr01  13981  rhmdvdsr  14052  lspf  14266  lspval  14267  lssats2  14291  fiinbas  14636  topbas  14654  clsval  14698  neiint  14732  neipsm  14741  opnneissb  14742  opnssneib  14743  innei  14750  restbasg  14755  lmconst  14803  iscnp4  14805  cncnpi  14815  cnconst2  14820  cnptoprest  14826  cnpdis  14829  neitx  14855  txcnp  14858  blssps  15014  blss  15015  blssexps  15016  blssex  15017  ssblex  15018  blin2  15019  neibl  15078  metss2  15085  bdmopn  15091  metrest  15093  metcnp3  15098  tgioo  15141  tgqioo  15142  addcncntoplem  15148  cnopnap  15198  dedekindeulemuub  15204  suplociccreex  15211  dedekindicclemuub  15213  ivthinclemlm  15221  ivthinclemum  15222  ivthinclemlopn  15223  ivthinclemuopn  15225  ivthreinc  15232  elply2  15322  reeff1oleme  15359  sin0pilem2  15369  sgmnncl  15575  dvdsppwf1o  15576  perfect  15588  bj-nn0suc0  16085  bj-inf2vnlem1  16105  nninfsellemeq  16153  nninfomnilem  16157  qdencn  16168  trirec0  16185