Theorem rspc 3155

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 2753	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2602	. . . 4 |- F/_ x A
3		nfv 1771	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 2013	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2527	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 326	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 3140	. . 3 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ( A e. B -> ps ) ) )
10	9	pm2.43a 51	. 2 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ps ) )
11	1, 10	syl5bi 225	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1452   = wceq 1454   F/wnf 1677   e. wcel 1897   A.wral 2748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-v 3058

This theorem is referenced by:  rspcv  3157  rspc2  3169  disjxiun  4412  pofun  4789  fmptcof  6080  fliftfuns  6231  ofmpteq  6576  qliftfuns  7475  xpf1o  7759  iunfi  7887  iundom2g  8990  lble  10585  rlimcld2  13690  sumeq2ii  13807  summolem3  13828  zsum  13832  fsum  13834  fsumf1o  13837  sumss2  13840  fsumcvg2  13841  fsumadd  13853  isummulc2  13871  fsum2dlem  13879  fsumcom2  13883  fsumshftm  13890  fsum0diag2  13892  fsummulc2  13893  fsum00  13906  fsumabs  13909  fsumrelem  13915  fsumrlim  13919  fsumo1  13920  o1fsum  13921  fsumiun  13929  isumshft  13945  prodeq2ii  14015  prodmolem3  14035  zprod  14039  fprod  14043  fprodf1o  14048  prodss  14049  fprodser  14051  fprodmul  14062  fproddiv  14063  fprodm1s  14072  fprodp1s  14073  fprodabs  14076  fprod2dlem  14082  fprodcom2  14086  fprodefsum  14197  pcmpt  14885  invfuc  15927  dprd2d2  17725  txcnp  20683  ptcnplem  20684  prdsdsf  21430  prdsxmet  21432  fsumcn  21950  ovolfiniun  22502  ovoliunnul  22508  volfiniun  22548  iunmbl  22554  limciun  22897  dvfsumle  23021  dvfsumabs  23023  dvfsumlem1  23026  dvfsumlem3  23028  dvfsumlem4  23029  dvfsumrlim  23031  dvfsumrlim2  23032  dvfsum2  23034  itgsubst  23049  fsumvma  24189  dchrisumlema  24374  dchrisumlem2  24376  dchrisumlem3  24377  chirred  28096  rspcda  28162  sigapildsyslem  29031  voliune  29100  volfiniune  29101  tfisg  30505  ptrest  31983  poimirlem25  32009  poimirlem26  32010  mzpsubst  35634  rabdiophlem2  35689  etransclem48OLD  38184  etransclem48  38185  sge0iunmpt  38297