Theorem rspc 3006

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)

Hypotheses

Ref	Expression
rspc.1	|- F/ x ps
rspc.2	|- ( x = A -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem rspc

Step	Hyp	Ref	Expression
1		df-ral 2671	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2540	. . . 4 |- F/_ x A
3		nfv 1626	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1828	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2464	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 312	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 2991	. . 3 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ( A e. B -> ps ) ) )
10	9	pm2.43a 47	. 2 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ps ) )
11	1, 10	syl5bi 209	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 177   A.wal 1546   F/wnf 1550   = wceq 1649   e. wcel 1721   A.wral 2666

This theorem is referenced by:  rspcv  3008  rspc2  3017  disjxiun  4169  pofun  4479  fmptcof  5861  fliftfuns  5995  qliftfuns  6950  xpf1o  7228  iunfi  7353  iundom2g  8371  lble  9916  rlimcld2  12327  sumeq2ii  12442  summolem3  12463  zsum  12467  fsum  12469  fsumf1o  12472  sumss2  12475  fsumcvg2  12476  fsumadd  12487  isummulc2  12501  fsum2dlem  12509  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsummulc2  12522  fsum00  12532  fsumabs  12535  fsumrelem  12541  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  isumshft  12574  pcmpt  13216  invfuc  14126  dprd2d2  15557  txcnp  17605  ptcnplem  17606  prdsdsf  18350  prdsxmet  18352  fsumcn  18853  ovolfiniun  19350  ovoliunnul  19356  volfiniun  19394  iunmbl  19400  limciun  19734  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim  19868  dvfsumrlim2  19869  dvfsum2  19871  itgsubst  19886  fsumvma  20950  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  chirred  23851  voliune  24538  volfiniune  24539  prodeq2ii  25192  prodmolem3  25212  zprod  25216  fprod  25220  fprodf1o  25225  prodss  25226  fprodser  25228  fprodmul  25237  fproddiv  25238  fprodm1s  25246  fprodp1s  25247  fprodabs  25250  fprodefsum  25251  fprod2dlem  25257  fprodcom2  25261  tfisg  25418  ofmpteq  26666  mzpsubst  26695  rabdiophlem2  26752

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918