Theorem rspcv 2838

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   e. wcel 2148   A.wral 2455

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-ral 2460  df-v 2740

This theorem is referenced by:  rspccv  2839  rspcva  2840  rspccva  2841  rspcdva  2847  rspc3v  2858  rr19.3v  2877  rr19.28v  2878  rspsbc  3046  rspc2vd  3126  intmin  3865  ralxfrALT  4468  ontr2exmid  4525  reg2exmidlema  4534  0elsucexmid  4565  funcnvuni  5286  acexmidlemcase  5870  tfrlem1  6309  tfrlem9  6320  oawordriexmid  6471  nneneq  6857  diffitest  6887  xpfi  6929  ordiso2  7034  exmidontriimlem3  7222  prnmaxl  7487  prnminu  7488  cauappcvgprlemm  7644  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgsrlemcl  7788  caucvgsrlemfv  7790  caucvgsr  7801  axcaucvglemres  7898  lbreu  8902  nnsub  8958  supinfneg  9595  infsupneg  9596  ublbneg  9613  fzrevral  10105  seq3caopr3  10481  seq3id3  10507  recan  11118  cau3lem  11123  caubnd2  11126  climshftlemg  11310  subcn2  11319  climcau  11355  serf0  11360  sumdc  11366  isumrpcl  11502  clim2prod  11547  prodmodclem2  11585  ndvdssub  11935  zsupcllemex  11947  dfgcd3  12011  dfgcd2  12015  coprmgcdb  12088  coprmdvds1  12091  nprm  12123  dvdsprm  12137  coprm  12144  sqrt2irr  12162  pcmpt  12341  pcmptdvds  12343  pcfac  12348  prmpwdvds  12353  lidrididd  12801  dfgrp2  12902  grpidinv2  12928  dfgrp3mlem  12968  issubg4m  13053  srgrz  13167  srglz  13168  srgisid  13169  islmodd  13383  rmodislmod  13441  cnpnei  13722  lmss  13749  txlm  13782  psmet0  13830  metss  13997  metcnp3  14014  mulc1cncf  14079  cncfco  14081  2sqlem6  14470  2sqlem10  14475  bj-indsuc  14683  bj-inf2vnlem2  14726  trirec0  14795  iswomni0  14802  neap0mkv  14819