Theorem rspc 2878

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 2491	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2350	. . . 4 |- F/_ x A
3		nfv 1552	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1596	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2270	. . . . 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 2862	. . 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 1371   = wceq 1373   F/wnf 1484   e. wcel 2178   A.wral 2486

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778

This theorem is referenced by:  rspcv  2880  rspc2  2895  rspc2vd  3170  pofun  4377  omsinds  4688  fmptcof  5770  fliftfuns  5890  qliftfuns  6729  xpf1o  6966  finexdc  7025  ssfirab  7059  opabfi  7061  iunfidisj  7074  dcfi  7109  cc3  7415  lble  9055  exfzdc  10406  zsupcllemstep  10409  infssuzex  10413  uzsinds  10626  sumeq2  11785  sumfct  11800  sumrbdclem  11803  summodclem3  11806  summodclem2a  11807  zsumdc  11810  fsumgcl  11812  fsum3  11813  fsumf1o  11816  isumss  11817  isumss2  11819  fsum3cvg2  11820  fsumadd  11832  isummulc2  11852  fsum2dlemstep  11860  fisumcom2  11864  fsumshftm  11871  fisum0diag2  11873  fsummulc2  11874  fsum00  11888  fsumabs  11891  fsumrelem  11897  fsumiun  11903  isumshft  11916  mertenslem2  11962  prodeq2  11983  prodrbdclem  11997  prodmodclem3  12001  prodmodclem2a  12002  zproddc  12005  fprodseq  12009  prodfct  12013  fprodf1o  12014  prodssdc  12015  fprodmul  12017  fprodm1s  12027  fprodp1s  12028  fprodabs  12042  fprodap0  12047  fprod2dlemstep  12048  fprodcom2fi  12052  fprodrec  12055  fprodap0f  12062  fprodle  12066  bezoutlemmain  12434  nnwosdc  12475  pcmpt  12781  ctiunctlemudc  12923  gsumfzfsumlemm  14464  iuncld  14702  txcnp  14858  fsumcncntop  15154  bj-nntrans  16086