Theorem rspcsbela 3814

Description: Special case related to rspsbc 3384. (Contributed by NM, 10-Dec-2005.) (Proof shortened by Eric Schmidt, 17-Jan-2007.)

Assertion

Ref	Expression
rspcsbela	|- ( ( A e. B /\ A. x e. B C e. D ) -> [_ A / x ]_ C e. D )

Distinct variable groups:   x, B   x, D

Allowed substitution hints:   A( x)   C( x)

Proof of Theorem rspcsbela

Step	Hyp	Ref	Expression
1		rspsbc 3384	. . 3 |- ( A e. B -> ( A. x e. B C e. D -> [. A / x ]. C e. D ) )
2		sbcel1g 3790	. . 3 |- ( A e. B -> ( [. A / x ]. C e. D <-> [_ A / x ]_ C e. D ) )
3	1, 2	sylibd 214	. 2 |- ( A e. B -> ( A. x e. B C e. D -> [_ A / x ]_ C e. D ) )
4	3	imp 429	1 |- ( ( A e. B /\ A. x e. B C e. D ) -> [_ A / x ]_ C e. D )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1758   A.wral 2799   [.wsbc 3294   [_csb 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-sbc 3295  df-csb 3397  df-dif 3440  df-in 3444  df-ss 3451  df-nul 3747

This theorem is referenced by:  gsummpt1n0  16579  mptscmfsupp0  17135  evl1gsumdlem  17916  madugsum  18582  iunmbl2  21172  gsumvsca1  26397  gsumvsca2  26398  fsumz  30385  fsummsndifre  30386  fsumsplitsndif  30387  fsummmodsndifre  30388  modfsummodslem1  30389  fsummsnunz  30390  fsumsplitsnun  30391  fsummmodsnunre  30392  mptnn0fsupp  30951  mptnn0fsuppr  30953  gsummptnn0fz  30959  telescfzgsumlem  30962  telescfzgsum  30963  telescgsum  30967  coe1fzgsumdlem  30991  gsummoncoe1  30997