Theorem rspcv 2903

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 26-May-1998.)

Hypothesis

Ref	Expression
rspcv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rspcv	|- ( A e. B -> ( A. x e. B ph -> ps ) )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem rspcv

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 |- F/ x ps
2		rspcv.1	. 2 |- ( x = A -> ( ph <-> ps ) )
3	1, 2	rspc 2901	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   e. wcel 2200   A.wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  rspccv  2904  rspcva  2905  rspccva  2906  rspcdva  2912  rspc3v  2923  rr19.3v  2942  rr19.28v  2943  rspsbc  3112  rspc2vd  3193  intmin  3943  ralxfrALT  4558  ontr2exmid  4617  reg2exmidlema  4626  0elsucexmid  4657  funcnvuni  5390  acexmidlemcase  6002  tfrlem1  6460  tfrlem9  6471  oawordriexmid  6624  nneneq  7026  diffitest  7057  xpfi  7105  ordiso2  7213  exmidontriimlem3  7416  prnmaxl  7686  prnminu  7687  cauappcvgprlemm  7843  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsr  8000  axcaucvglemres  8097  lbreu  9103  nnsub  9160  supinfneg  9802  infsupneg  9803  ublbneg  9820  fzrevral  10313  zsupcllemex  10462  seq3caopr3  10725  seq3id3  10758  ccatalpha  11161  wrdind  11270  wrd2ind  11271  reuccatpfxs1lem  11294  recan  11636  cau3lem  11641  caubnd2  11644  climshftlemg  11829  subcn2  11838  climcau  11874  serf0  11879  sumdc  11885  isumrpcl  12021  clim2prod  12066  prodmodclem2  12104  ndvdssub  12457  dfgcd3  12547  dfgcd2  12551  coprmgcdb  12626  coprmdvds1  12629  nprm  12661  dvdsprm  12675  coprm  12682  sqrt2irr  12700  pcmpt  12882  pcmptdvds  12884  pcfac  12889  prmpwdvds  12894  lidrididd  13431  dfgrp2  13576  grpidinv2  13607  dfgrp3mlem  13647  issubg4m  13746  srgrz  13963  srglz  13964  srgisid  13965  rrgeq0i  14244  islmodd  14273  rmodislmod  14331  rnglidlmcl  14460  cnpnei  14909  lmss  14936  txlm  14969  psmet0  15017  metss  15184  metcnp3  15201  mulc1cncf  15279  cncfco  15281  2sqlem6  15815  2sqlem10  15820  usgruspgrben  16000  wlk1walkdom  16105  wlkres  16123  clwwlkccatlem  16143  clwwlkext2edg  16164  bj-indsuc  16374  bj-inf2vnlem2  16417  pw1dceq  16457  trirec0  16500  iswomni0  16507  neap0mkv  16525