Theorem rspc 3166

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 2800	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2613	. . . 4 |- F/_ x A
3		nfv 1674	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1855	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2523	. . . . 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 3151	. . 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 1368   = wceq 1370   F/wnf 1590   e. wcel 1758   A.wral 2795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3073

This theorem is referenced by:  rspcv  3168  rspc2  3178  disjxiun  4390  pofun  4758  fmptcof  5979  fliftfuns  6109  ofmpteq  6441  qliftfuns  7290  xpf1o  7576  iunfi  7703  iundom2g  8808  lble  10386  rlimcld2  13167  sumeq2ii  13281  summolem3  13302  zsum  13306  fsum  13308  fsumf1o  13311  sumss2  13314  fsumcvg2  13315  fsumadd  13326  isummulc2  13340  fsum2dlem  13348  fsumcom2  13352  fsumshftm  13359  fsum0diag2  13361  fsummulc2  13362  fsum00  13372  fsumabs  13375  fsumrelem  13381  fsumrlim  13385  fsumo1  13386  o1fsum  13387  fsumiun  13395  isumshft  13413  pcmpt  14065  invfuc  14995  dprd2d2  16657  txcnp  19318  ptcnplem  19319  prdsdsf  20067  prdsxmet  20069  fsumcn  20571  ovolfiniun  21109  ovoliunnul  21115  volfiniun  21154  iunmbl  21160  limciun  21495  dvfsumle  21619  dvfsumabs  21621  dvfsumlem1  21624  dvfsumlem3  21626  dvfsumlem4  21627  dvfsumrlim  21629  dvfsumrlim2  21630  dvfsum2  21632  itgsubst  21647  fsumvma  22678  dchrisumlema  22863  dchrisumlem2  22865  dchrisumlem3  22866  chirred  25944  nn0min  26228  voliune  26782  volfiniune  26783  prodeq2ii  27563  prodmolem3  27583  zprod  27587  fprod  27591  fprodf1o  27596  prodss  27597  fprodser  27599  fprodmul  27608  fproddiv  27609  fprodm1s  27617  fprodp1s  27618  fprodabs  27621  fprodefsum  27622  fprod2dlem  27628  fprodcom2  27632  tfisg  27802  ptrest  28566  mzpsubst  29226  rabdiophlem2  29281