Theorem rspc 2904

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 2515	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2374	. . . 4 |- F/_ x A
3		nfv 1576	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1620	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2294	. . . . 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 2888	. . 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 1395   = wceq 1397   F/wnf 1508   e. wcel 2202   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804

This theorem is referenced by:  rspcv  2906  rspc2  2921  rspc2vd  3196  pofun  4409  omsinds  4720  fmptcof  5814  fliftfuns  5938  qliftfuns  6787  xpf1o  7029  finexdc  7091  ssfirab  7128  opabfi  7131  iunfidisj  7144  dcfi  7179  cc3  7486  lble  9126  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  uzsinds  10705  sumeq2  11919  sumfct  11934  sumrbdclem  11937  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  fsumf1o  11950  isumss  11951  isumss2  11953  fsum3cvg2  11954  fsumadd  11966  isummulc2  11986  fsum2dlemstep  11994  fisumcom2  11998  fsumshftm  12005  fisum0diag2  12007  fsummulc2  12008  fsum00  12022  fsumabs  12025  fsumrelem  12031  fsumiun  12037  isumshft  12050  mertenslem2  12096  prodeq2  12117  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  prodfct  12147  fprodf1o  12148  prodssdc  12149  fprodmul  12151  fprodm1s  12161  fprodp1s  12162  fprodabs  12176  fprodap0  12181  fprod2dlemstep  12182  fprodcom2fi  12186  fprodrec  12189  fprodap0f  12196  fprodle  12200  bezoutlemmain  12568  nnwosdc  12609  pcmpt  12915  ctiunctlemudc  13057  gsumfzfsumlemm  14600  iuncld  14838  txcnp  14994  fsumcncntop  15290  bj-nntrans  16546