Theorem rspc 2905

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 2516	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2375	. . . 4 |- F/_ x A
3		nfv 1577	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1621	. . . 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 2889	. . 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 1396   = wceq 1398   F/wnf 1509   e. wcel 2202   A.wral 2511

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805

This theorem is referenced by:  rspcv  2907  rspc2  2922  rspc2vd  3197  pofun  4415  omsinds  4726  fmptcof  5822  fliftfuns  5949  qliftfuns  6831  xpf1o  7073  finexdc  7135  ssfirab  7172  opabfi  7175  iunfidisj  7188  dcfi  7223  cc3  7530  lble  9169  exfzdc  10532  zsupcllemstep  10535  infssuzex  10539  uzsinds  10752  sumeq2  11982  sumfct  11997  sumrbdclem  12001  summodclem3  12004  summodclem2a  12005  zsumdc  12008  fsumgcl  12010  fsum3  12011  fsumf1o  12014  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsumadd  12030  isummulc2  12050  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fisum0diag2  12071  fsummulc2  12072  fsum00  12086  fsumabs  12089  fsumrelem  12095  fsumiun  12101  isumshft  12114  mertenslem2  12160  prodeq2  12181  prodrbdclem  12195  prodmodclem3  12199  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  prodfct  12211  fprodf1o  12212  prodssdc  12213  fprodmul  12215  fprodm1s  12225  fprodp1s  12226  fprodabs  12240  fprodap0  12245  fprod2dlemstep  12246  fprodcom2fi  12250  fprodrec  12253  fprodap0f  12260  fprodle  12264  bezoutlemmain  12632  nnwosdc  12673  pcmpt  12979  ctiunctlemudc  13121  gsumfzfsumlemm  14666  iuncld  14909  txcnp  15065  fsumcncntop  15361  bj-nntrans  16650