Theorem rspc 2717

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 2365	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2229	. . . 4 |- F/_ x A
3		nfv 1467	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1510	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2151	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 233	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 2702	. . 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	syl5bi 151	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1288   = wceq 1290   F/wnf 1395   e. wcel 1439   A.wral 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-v 2622

This theorem is referenced by:  rspcv  2719  rspc2  2733  pofun  4148  omsinds  4448  fmptcof  5479  fliftfuns  5591  qliftfuns  6390  xpf1o  6614  finexdc  6672  ssfirab  6697  iunfidisj  6709  lble  8469  exfzdc  9712  uzsinds  9909  sumeq2  10809  sumfct  10824  isumrblem  10826  isummolem3  10831  isummolem2a  10832  zisum  10835  fsumgcl  10838  fisum  10839  fsumf1o  10843  isumss  10844  isumss2  10846  fisumcvg2  10847  fsum3cvg2  10848  fsumadd  10861  isummulc2  10881  fsum2dlemstep  10889  fisumcom2  10893  fsumshftm  10900  fisum0diag2  10902  fsummulc2  10903  fsum00  10917  fsumabs  10920  fsumrelem  10926  fsumiun  10932  isumshft  10945  mertenslem2  10991  zsupcllemstep  11280  infssuzex  11284  bezoutlemmain  11326  iuncld  11876  bj-nntrans  12119