Theorem rspc 2833

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 2458	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2317	. . . 4 |- F/_ x A
3		nfv 1526	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1570	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2238	. . . . 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 2817	. . 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 1351   = wceq 1353   F/wnf 1458   e. wcel 2146   A.wral 2453

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737

This theorem is referenced by:  rspcv  2835  rspc2  2850  rspc2vd  3123  pofun  4306  omsinds  4615  fmptcof  5675  fliftfuns  5789  qliftfuns  6609  xpf1o  6834  finexdc  6892  ssfirab  6923  iunfidisj  6935  dcfi  6970  cc3  7242  lble  8877  exfzdc  10210  uzsinds  10412  sumeq2  11335  sumfct  11350  sumrbdclem  11353  summodclem3  11356  summodclem2a  11357  zsumdc  11360  fsumgcl  11362  fsum3  11363  fsumf1o  11366  isumss  11367  isumss2  11369  fsum3cvg2  11370  fsumadd  11382  isummulc2  11402  fsum2dlemstep  11410  fisumcom2  11414  fsumshftm  11421  fisum0diag2  11423  fsummulc2  11424  fsum00  11438  fsumabs  11441  fsumrelem  11447  fsumiun  11453  isumshft  11466  mertenslem2  11512  prodeq2  11533  prodrbdclem  11547  prodmodclem3  11551  prodmodclem2a  11552  zproddc  11555  fprodseq  11559  prodfct  11563  fprodf1o  11564  prodssdc  11565  fprodmul  11567  fprodm1s  11577  fprodp1s  11578  fprodabs  11592  fprodap0  11597  fprod2dlemstep  11598  fprodcom2fi  11602  fprodrec  11605  fprodap0f  11612  fprodle  11616  zsupcllemstep  11913  infssuzex  11917  bezoutlemmain  11966  nnwosdc  12007  pcmpt  12308  ctiunctlemudc  12405  iuncld  13195  txcnp  13351  fsumcncntop  13636  bj-nntrans  14272