Theorem rspc 2902

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 2886	. . 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 2802

This theorem is referenced by:  rspcv  2904  rspc2  2919  rspc2vd  3194  pofun  4407  omsinds  4718  fmptcof  5810  fliftfuns  5934  qliftfuns  6783  xpf1o  7025  finexdc  7085  ssfirab  7121  opabfi  7123  iunfidisj  7136  dcfi  7171  cc3  7477  lble  9117  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  uzsinds  10696  sumeq2  11910  sumfct  11925  sumrbdclem  11928  summodclem3  11931  summodclem2a  11932  zsumdc  11935  fsumgcl  11937  fsum3  11938  fsumf1o  11941  isumss  11942  isumss2  11944  fsum3cvg2  11945  fsumadd  11957  isummulc2  11977  fsum2dlemstep  11985  fisumcom2  11989  fsumshftm  11996  fisum0diag2  11998  fsummulc2  11999  fsum00  12013  fsumabs  12016  fsumrelem  12022  fsumiun  12028  isumshft  12041  mertenslem2  12087  prodeq2  12108  prodrbdclem  12122  prodmodclem3  12126  prodmodclem2a  12127  zproddc  12130  fprodseq  12134  prodfct  12138  fprodf1o  12139  prodssdc  12140  fprodmul  12142  fprodm1s  12152  fprodp1s  12153  fprodabs  12167  fprodap0  12172  fprod2dlemstep  12173  fprodcom2fi  12177  fprodrec  12180  fprodap0f  12187  fprodle  12191  bezoutlemmain  12559  nnwosdc  12600  pcmpt  12906  ctiunctlemudc  13048  gsumfzfsumlemm  14591  iuncld  14829  txcnp  14985  fsumcncntop  15281  bj-nntrans  16482