Theorem rspc 2807

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 2437	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2296	. . . 4 |- F/_ x A
3		nfv 1505	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1549	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2217	. . . . 5 |- ( x = A -> ( x e. B <-> A e. B ) )
7		rspc.2	. . . . 5 |- ( x = A -> ( ph <-> ps ) )
8	6, 7	imbi12d 233	. . . 4 |- ( x = A -> ( ( x e. B -> ph ) <-> ( A e. B -> ps ) ) )
9	2, 5, 8	spcgf 2791	. . 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	syl5bi 151	1 |- ( A e. B -> ( A. x e. B ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1330   = wceq 1332   F/wnf 1437   e. wcel 2125   A.wral 2432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-v 2711

This theorem is referenced by:  rspcv  2809  rspc2  2824  pofun  4267  omsinds  4575  fmptcof  5627  fliftfuns  5739  qliftfuns  6553  xpf1o  6778  finexdc  6836  ssfirab  6867  iunfidisj  6879  cc3  7167  lble  8797  exfzdc  10117  uzsinds  10319  sumeq2  11233  sumfct  11248  sumrbdclem  11251  summodclem3  11254  summodclem2a  11255  zsumdc  11258  fsumgcl  11260  fsum3  11261  fsumf1o  11264  isumss  11265  isumss2  11267  fsum3cvg2  11268  fsumadd  11280  isummulc2  11300  fsum2dlemstep  11308  fisumcom2  11312  fsumshftm  11319  fisum0diag2  11321  fsummulc2  11322  fsum00  11336  fsumabs  11339  fsumrelem  11345  fsumiun  11351  isumshft  11364  mertenslem2  11410  prodeq2  11431  prodrbdclem  11445  prodmodclem3  11449  prodmodclem2a  11450  zproddc  11453  fprodseq  11457  prodfct  11461  fprodf1o  11462  prodssdc  11463  fprodmul  11465  fprodm1s  11475  fprodp1s  11476  fprodabs  11490  fprodap0  11495  fprod2dlemstep  11496  fprodcom2fi  11500  fprodrec  11503  fprodap0f  11510  fprodle  11514  zsupcllemstep  11805  infssuzex  11809  bezoutlemmain  11853  ctiunctlemudc  12117  iuncld  12454  txcnp  12610  fsumcncntop  12895  bj-nntrans  13464