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  4402  omsinds  4713  fmptcof  5801  fliftfuns  5921  qliftfuns  6764  xpf1o  7001  finexdc  7060  ssfirab  7094  opabfi  7096  iunfidisj  7109  dcfi  7144  cc3  7450  lble  9090  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  uzsinds  10661  sumeq2  11865  sumfct  11880  sumrbdclem  11883  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  fsumf1o  11896  isumss  11897  isumss2  11899  fsum3cvg2  11900  fsumadd  11912  isummulc2  11932  fsum2dlemstep  11940  fisumcom2  11944  fsumshftm  11951  fisum0diag2  11953  fsummulc2  11954  fsum00  11968  fsumabs  11971  fsumrelem  11977  fsumiun  11983  isumshft  11996  mertenslem2  12042  prodeq2  12063  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  prodfct  12093  fprodf1o  12094  prodssdc  12095  fprodmul  12097  fprodm1s  12107  fprodp1s  12108  fprodabs  12122  fprodap0  12127  fprod2dlemstep  12128  fprodcom2fi  12132  fprodrec  12135  fprodap0f  12142  fprodle  12146  bezoutlemmain  12514  nnwosdc  12555  pcmpt  12861  ctiunctlemudc  13003  gsumfzfsumlemm  14545  iuncld  14783  txcnp  14939  fsumcncntop  15235  bj-nntrans  16272