Theorem rspc 3062

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 2715	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2574	. . . 4 |- F/_ x A
3		nfv 1673	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1852	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2498	. . . . 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 3047	. . 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 1367   = wceq 1369   F/wnf 1589   e. wcel 1756   A.wral 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969

This theorem is referenced by:  rspcv  3064  rspc2  3073  disjxiun  4284  pofun  4652  fmptcof  5872  fliftfuns  6002  ofmpteq  6333  qliftfuns  7179  xpf1o  7465  iunfi  7591  iundom2g  8696  lble  10274  rlimcld2  13048  sumeq2ii  13162  summolem3  13183  zsum  13187  fsum  13189  fsumf1o  13192  sumss2  13195  fsumcvg2  13196  fsumadd  13207  isummulc2  13221  fsum2dlem  13229  fsumcom2  13233  fsumshftm  13240  fsum0diag2  13242  fsummulc2  13243  fsum00  13253  fsumabs  13256  fsumrelem  13262  fsumrlim  13266  fsumo1  13267  o1fsum  13268  fsumiun  13276  isumshft  13294  pcmpt  13946  invfuc  14876  dprd2d2  16531  txcnp  19168  ptcnplem  19169  prdsdsf  19917  prdsxmet  19919  fsumcn  20421  ovolfiniun  20959  ovoliunnul  20965  volfiniun  21003  iunmbl  21009  limciun  21344  dvfsumle  21468  dvfsumabs  21470  dvfsumlem1  21473  dvfsumlem3  21475  dvfsumlem4  21476  dvfsumrlim  21478  dvfsumrlim2  21479  dvfsum2  21481  itgsubst  21496  fsumvma  22527  dchrisumlema  22712  dchrisumlem2  22714  dchrisumlem3  22715  chirred  25750  nn0min  26041  voliune  26597  volfiniune  26598  prodeq2ii  27377  prodmolem3  27397  zprod  27401  fprod  27405  fprodf1o  27410  prodss  27411  fprodser  27413  fprodmul  27422  fproddiv  27423  fprodm1s  27431  fprodp1s  27432  fprodabs  27435  fprodefsum  27436  fprod2dlem  27442  fprodcom2  27446  tfisg  27616  ptrest  28378  mzpsubst  29038  rabdiophlem2  29093