Theorem rspc 2923

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 2533	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2392	. . . 4 |- F/_ x A
3		nfv 1581	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1625	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2301	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 234	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 2907	. . 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	biimtrid 152	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1400   = wceq 1402   F/wnf 1513   e. wcel 2209   A.wral 2528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823

This theorem is referenced by:  rspcv  2925  rspc2  2941  rspc2vd  3216  pofun  4452  omsinds  4764  fmptcof  5866  fliftfuns  5994  qliftfuns  6883  xpf1o  7134  finexdc  7197  ssfirab  7234  opabfi  7237  iunfidisj  7250  dcfi  7305  cc3  7624  lble  9267  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  uzsinds  10859  sumeq2  12103  sumfct  12118  sumrbdclem  12122  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  fsumf1o  12135  isumss  12136  isumss2  12138  fsum3cvg2  12139  fsumadd  12151  isummulc2  12171  fsum2dlemstep  12179  fisumcom2  12183  fsumshftm  12190  fisum0diag2  12192  fsummulc2  12193  fsum00  12207  fsumabs  12210  fsumrelem  12216  fsumiun  12222  isumshft  12235  mertenslem2  12281  prodeq2  12302  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  prodfct  12332  fprodf1o  12333  prodssdc  12334  fprodmul  12336  fprodm1s  12346  fprodp1s  12347  fprodabs  12361  fprodap0  12366  fprod2dlemstep  12367  fprodcom2fi  12371  fprodrec  12374  fprodap0f  12381  fprodle  12385  bezoutlemmain  12753  nnwosdc  12794  pcmpt  13100  ctiunctlemudc  13306  gsummptfidmadd  14138  iuncld  15139  txcnp  15295  fsumcncntop  15591  bj-nntrans  16891