Theorem rspc 2901

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 2513	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2372	. . . 4 |- F/_ x A
3		nfv 1574	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1618	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2292	. . . . 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 2885	. . 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 1393   = wceq 1395   F/wnf 1506   e. wcel 2200   A.wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801

This theorem is referenced by:  rspcv  2903  rspc2  2918  rspc2vd  3193  pofun  4403  omsinds  4714  fmptcof  5804  fliftfuns  5928  qliftfuns  6774  xpf1o  7013  finexdc  7073  ssfirab  7109  opabfi  7111  iunfidisj  7124  dcfi  7159  cc3  7465  lble  9105  exfzdc  10458  zsupcllemstep  10461  infssuzex  10465  uzsinds  10678  sumeq2  11885  sumfct  11900  sumrbdclem  11903  summodclem3  11906  summodclem2a  11907  zsumdc  11910  fsumgcl  11912  fsum3  11913  fsumf1o  11916  isumss  11917  isumss2  11919  fsum3cvg2  11920  fsumadd  11932  isummulc2  11952  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fisum0diag2  11973  fsummulc2  11974  fsum00  11988  fsumabs  11991  fsumrelem  11997  fsumiun  12003  isumshft  12016  mertenslem2  12062  prodeq2  12083  prodrbdclem  12097  prodmodclem3  12101  prodmodclem2a  12102  zproddc  12105  fprodseq  12109  prodfct  12113  fprodf1o  12114  prodssdc  12115  fprodmul  12117  fprodm1s  12127  fprodp1s  12128  fprodabs  12142  fprodap0  12147  fprod2dlemstep  12148  fprodcom2fi  12152  fprodrec  12155  fprodap0f  12162  fprodle  12166  bezoutlemmain  12534  nnwosdc  12575  pcmpt  12881  ctiunctlemudc  13023  gsumfzfsumlemm  14566  iuncld  14804  txcnp  14960  fsumcncntop  15256  bj-nntrans  16369