Theorem rspcv 2880

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   e. wcel 2178   A.wral 2486

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-ral 2491  df-v 2778

This theorem is referenced by:  rspccv  2881  rspcva  2882  rspccva  2883  rspcdva  2889  rspc3v  2900  rr19.3v  2919  rr19.28v  2920  rspsbc  3089  rspc2vd  3170  intmin  3919  ralxfrALT  4532  ontr2exmid  4591  reg2exmidlema  4600  0elsucexmid  4631  funcnvuni  5362  acexmidlemcase  5962  tfrlem1  6417  tfrlem9  6428  oawordriexmid  6579  nneneq  6979  diffitest  7010  xpfi  7055  ordiso2  7163  exmidontriimlem3  7366  prnmaxl  7636  prnminu  7637  cauappcvgprlemm  7793  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgsrlemcl  7937  caucvgsrlemfv  7939  caucvgsr  7950  axcaucvglemres  8047  lbreu  9053  nnsub  9110  supinfneg  9751  infsupneg  9752  ublbneg  9769  fzrevral  10262  zsupcllemex  10410  seq3caopr3  10673  seq3id3  10706  wrdind  11213  wrd2ind  11214  reuccatpfxs1lem  11237  recan  11535  cau3lem  11540  caubnd2  11543  climshftlemg  11728  subcn2  11737  climcau  11773  serf0  11778  sumdc  11784  isumrpcl  11920  clim2prod  11965  prodmodclem2  12003  ndvdssub  12356  dfgcd3  12446  dfgcd2  12450  coprmgcdb  12525  coprmdvds1  12528  nprm  12560  dvdsprm  12574  coprm  12581  sqrt2irr  12599  pcmpt  12781  pcmptdvds  12783  pcfac  12788  prmpwdvds  12793  lidrididd  13329  dfgrp2  13474  grpidinv2  13505  dfgrp3mlem  13545  issubg4m  13644  srgrz  13861  srglz  13862  srgisid  13863  rrgeq0i  14141  islmodd  14170  rmodislmod  14228  rnglidlmcl  14357  cnpnei  14806  lmss  14833  txlm  14866  psmet0  14914  metss  15081  metcnp3  15098  mulc1cncf  15176  cncfco  15178  2sqlem6  15712  2sqlem10  15717  bj-indsuc  16063  bj-inf2vnlem2  16106  trirec0  16185  iswomni0  16192  neap0mkv  16210