Theorem rspc 2862

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 2480	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2339	. . . 4 |- F/_ x A
3		nfv 1542	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1586	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2259	. . . . 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 2846	. . 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 1362   = wceq 1364   F/wnf 1474   e. wcel 2167   A.wral 2475

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765

This theorem is referenced by:  rspcv  2864  rspc2  2879  rspc2vd  3153  pofun  4348  omsinds  4659  fmptcof  5732  fliftfuns  5848  qliftfuns  6687  xpf1o  6914  finexdc  6972  ssfirab  7006  opabfi  7008  iunfidisj  7021  dcfi  7056  cc3  7351  lble  8991  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  uzsinds  10553  sumeq2  11541  sumfct  11556  sumrbdclem  11559  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsumgcl  11568  fsum3  11569  fsumf1o  11572  isumss  11573  isumss2  11575  fsum3cvg2  11576  fsumadd  11588  isummulc2  11608  fsum2dlemstep  11616  fisumcom2  11620  fsumshftm  11627  fisum0diag2  11629  fsummulc2  11630  fsum00  11644  fsumabs  11647  fsumrelem  11653  fsumiun  11659  isumshft  11672  mertenslem2  11718  prodeq2  11739  prodrbdclem  11753  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  prodfct  11769  fprodf1o  11770  prodssdc  11771  fprodmul  11773  fprodm1s  11783  fprodp1s  11784  fprodabs  11798  fprodap0  11803  fprod2dlemstep  11804  fprodcom2fi  11808  fprodrec  11811  fprodap0f  11818  fprodle  11822  bezoutlemmain  12190  nnwosdc  12231  pcmpt  12537  ctiunctlemudc  12679  gsumfzfsumlemm  14219  iuncld  14435  txcnp  14591  fsumcncntop  14887  bj-nntrans  15681