Theorem rspc 3208

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 2819	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2629	. . . 4 |- F/_ x A
3		nfv 1683	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1867	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2539	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 320	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 3193	. . 3 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ( A e. B -> ps ) ) )
10	9	pm2.43a 49	. 2 |- ( A e. B -> ( A. x ( x e. B -> ph ) -> ps ) )
11	1, 10	syl5bi 217	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1377   = wceq 1379   F/wnf 1599   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115

This theorem is referenced by:  rspcv  3210  rspc2  3222  disjxiun  4444  pofun  4816  fmptcof  6053  fliftfuns  6198  ofmpteq  6540  qliftfuns  7395  xpf1o  7676  iunfi  7804  iundom2g  8911  lble  10491  rlimcld2  13360  sumeq2ii  13474  summolem3  13495  zsum  13499  fsum  13501  fsumf1o  13504  sumss2  13507  fsumcvg2  13508  fsumadd  13520  isummulc2  13536  fsum2dlem  13544  fsumcom2  13548  fsumshftm  13555  fsum0diag2  13557  fsummulc2  13558  fsum00  13571  fsumabs  13574  fsumrelem  13580  fsumrlim  13584  fsumo1  13585  o1fsum  13586  fsumiun  13594  isumshft  13610  pcmpt  14266  invfuc  15197  dprd2d2  16883  txcnp  19856  ptcnplem  19857  prdsdsf  20605  prdsxmet  20607  fsumcn  21109  ovolfiniun  21647  ovoliunnul  21653  volfiniun  21692  iunmbl  21698  limciun  22033  dvfsumle  22157  dvfsumabs  22159  dvfsumlem1  22162  dvfsumlem3  22164  dvfsumlem4  22165  dvfsumrlim  22167  dvfsumrlim2  22168  dvfsum2  22170  itgsubst  22185  fsumvma  23216  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  chirred  26990  nn0min  27279  voliune  27841  volfiniune  27842  prodeq2ii  28622  prodmolem3  28642  zprod  28646  fprod  28650  fprodf1o  28655  prodss  28656  fprodser  28658  fprodmul  28667  fproddiv  28668  fprodm1s  28676  fprodp1s  28677  fprodabs  28680  fprodefsum  28681  fprod2dlem  28687  fprodcom2  28691  tfisg  28861  ptrest  29625  mzpsubst  30285  rabdiophlem2  30339  limcrecl  31171