Theorem rspc 2915

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 2525	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2384	. . . 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 2295	. . . . 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 2899	. . 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 2203   A.wral 2520

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 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815

This theorem is referenced by:  rspcv  2917  rspc2  2932  rspc2vd  3207  pofun  4433  omsinds  4744  fmptcof  5844  fliftfuns  5971  qliftfuns  6853  xpf1o  7097  finexdc  7160  ssfirab  7197  opabfi  7200  iunfidisj  7213  dcfi  7268  cc3  7582  lble  9221  exfzdc  10586  zsupcllemstep  10589  infssuzex  10593  uzsinds  10806  sumeq2  12044  sumfct  12059  sumrbdclem  12063  summodclem3  12066  summodclem2a  12067  zsumdc  12070  fsumgcl  12072  fsum3  12073  fsumf1o  12076  isumss  12077  isumss2  12079  fsum3cvg2  12080  fsumadd  12092  isummulc2  12112  fsum2dlemstep  12120  fisumcom2  12124  fsumshftm  12131  fisum0diag2  12133  fsummulc2  12134  fsum00  12148  fsumabs  12151  fsumrelem  12157  fsumiun  12163  isumshft  12176  mertenslem2  12222  prodeq2  12243  prodrbdclem  12257  prodmodclem3  12261  prodmodclem2a  12262  zproddc  12265  fprodseq  12269  prodfct  12273  fprodf1o  12274  prodssdc  12275  fprodmul  12277  fprodm1s  12287  fprodp1s  12288  fprodabs  12302  fprodap0  12307  fprod2dlemstep  12308  fprodcom2fi  12312  fprodrec  12315  fprodap0f  12322  fprodle  12326  bezoutlemmain  12694  nnwosdc  12735  pcmpt  13041  ctiunctlemudc  13188  gsumfzfsumlemm  14735  iuncld  14980  txcnp  15136  fsumcncntop  15432  bj-nntrans  16721