Theorem rspc 3190

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 2798	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2605	. . . 4 |- F/_ x A
3		nfv 1694	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1906	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2515	. . . . 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 3175	. . 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 1381   = wceq 1383   F/wnf 1603   e. wcel 1804   A.wral 2793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097

This theorem is referenced by:  rspcv  3192  rspc2  3204  disjxiun  4434  pofun  4806  fmptcof  6050  fliftfuns  6197  ofmpteq  6543  qliftfuns  7400  xpf1o  7681  iunfi  7810  iundom2g  8918  lble  10502  rlimcld2  13382  sumeq2ii  13496  summolem3  13517  zsum  13521  fsum  13523  fsumf1o  13526  sumss2  13529  fsumcvg2  13530  fsumadd  13542  isummulc2  13558  fsum2dlem  13566  fsumcom2  13570  fsumshftm  13577  fsum0diag2  13579  fsummulc2  13580  fsum00  13593  fsumabs  13596  fsumrelem  13602  fsumrlim  13606  fsumo1  13607  o1fsum  13608  fsumiun  13616  isumshft  13632  prodeq2ii  13701  prodmolem3  13721  zprod  13725  fprod  13729  fprodf1o  13734  prodss  13735  fprodser  13737  fprodmul  13746  fproddiv  13747  fprodm1s  13755  fprodp1s  13756  fprodabs  13759  fprod2dlem  13765  fprodcom2  13769  fprodefsum  13811  pcmpt  14392  invfuc  15321  dprd2d2  17071  txcnp  20098  ptcnplem  20099  prdsdsf  20847  prdsxmet  20849  fsumcn  21351  ovolfiniun  21889  ovoliunnul  21895  volfiniun  21934  iunmbl  21940  limciun  22275  dvfsumle  22399  dvfsumabs  22401  dvfsumlem1  22404  dvfsumlem3  22406  dvfsumlem4  22407  dvfsumrlim  22409  dvfsumrlim2  22410  dvfsum2  22412  itgsubst  22427  fsumvma  23464  dchrisumlema  23649  dchrisumlem2  23651  dchrisumlem3  23652  chirred  27290  voliune  28178  volfiniune  28179  tfisg  29259  ptrest  30023  mzpsubst  30656  rabdiophlem2  30710