Theorem rspc 2836

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 2460	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2319	. . . 4 |- F/_ x A
3		nfv 1528	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1572	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2240	. . . . 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 2820	. . 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 1460   e. wcel 2148   A.wral 2455

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740

This theorem is referenced by:  rspcv  2838  rspc2  2853  rspc2vd  3126  pofun  4313  omsinds  4622  fmptcof  5684  fliftfuns  5799  qliftfuns  6619  xpf1o  6844  finexdc  6902  ssfirab  6933  iunfidisj  6945  dcfi  6980  cc3  7267  lble  8904  exfzdc  10240  uzsinds  10442  sumeq2  11367  sumfct  11382  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  zsumdc  11392  fsumgcl  11394  fsum3  11395  fsumf1o  11398  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsumadd  11414  isummulc2  11434  fsum2dlemstep  11442  fisumcom2  11446  fsumshftm  11453  fisum0diag2  11455  fsummulc2  11456  fsum00  11470  fsumabs  11473  fsumrelem  11479  fsumiun  11485  isumshft  11498  mertenslem2  11544  prodeq2  11565  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  zproddc  11587  fprodseq  11591  prodfct  11595  fprodf1o  11596  prodssdc  11597  fprodmul  11599  fprodm1s  11609  fprodp1s  11610  fprodabs  11624  fprodap0  11629  fprod2dlemstep  11630  fprodcom2fi  11634  fprodrec  11637  fprodap0f  11644  fprodle  11648  zsupcllemstep  11946  infssuzex  11950  bezoutlemmain  11999  nnwosdc  12040  pcmpt  12341  ctiunctlemudc  12438  iuncld  13618  txcnp  13774  fsumcncntop  14059  bj-nntrans  14706