Theorem rspc 2871

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 2489	. 2 |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) )
2		nfcv 2348	. . . 4 |- F/_ x A
3		nfv 1551	. . . . 5 |- F/ x A e. B
4		rspc.1	. . . . 5 |- F/ x ps
5	3, 4	nfim 1595	. . . 4 |- F/ x ( A e. B -> ps )
6		eleq1 2268	. . . . 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 2855	. . 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 1483   e. wcel 2176   A.wral 2484

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-v 2774

This theorem is referenced by:  rspcv  2873  rspc2  2888  rspc2vd  3162  pofun  4359  omsinds  4670  fmptcof  5747  fliftfuns  5867  qliftfuns  6706  xpf1o  6941  finexdc  6999  ssfirab  7033  opabfi  7035  iunfidisj  7048  dcfi  7083  cc3  7380  lble  9020  exfzdc  10369  zsupcllemstep  10372  infssuzex  10376  uzsinds  10589  sumeq2  11670  sumfct  11685  sumrbdclem  11688  summodclem3  11691  summodclem2a  11692  zsumdc  11695  fsumgcl  11697  fsum3  11698  fsumf1o  11701  isumss  11702  isumss2  11704  fsum3cvg2  11705  fsumadd  11717  isummulc2  11737  fsum2dlemstep  11745  fisumcom2  11749  fsumshftm  11756  fisum0diag2  11758  fsummulc2  11759  fsum00  11773  fsumabs  11776  fsumrelem  11782  fsumiun  11788  isumshft  11801  mertenslem2  11847  prodeq2  11868  prodrbdclem  11882  prodmodclem3  11886  prodmodclem2a  11887  zproddc  11890  fprodseq  11894  prodfct  11898  fprodf1o  11899  prodssdc  11900  fprodmul  11902  fprodm1s  11912  fprodp1s  11913  fprodabs  11927  fprodap0  11932  fprod2dlemstep  11933  fprodcom2fi  11937  fprodrec  11940  fprodap0f  11947  fprodle  11951  bezoutlemmain  12319  nnwosdc  12360  pcmpt  12666  ctiunctlemudc  12808  gsumfzfsumlemm  14349  iuncld  14587  txcnp  14743  fsumcncntop  15039  bj-nntrans  15887