Theorem rspcsbela 3853

Description: Special case related to rspsbc 3421. (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 3421	. . 3 |- ( A e. B -> ( A. x e. B C e. D -> [. A / x ]. C e. D ) )
2		sbcel1g 3829	. . 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 1767   A.wral 2814   [.wsbc 3331   [_csb 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786

This theorem is referenced by:  mptnn0fsupp  12066  mptnn0fsuppr  12068  fsumzcl2  13516  fsummsnunz  13525  fsumsplitsnun  13526  modfsummodslem1  13562  gsummpt1n0  16780  gsummptnn0fz  16802  telgsumfzslem  16805  telgsumfzs  16806  telgsums  16810  mptscmfsupp0  17356  coe1fzgsumdlem  18111  gsummoncoe1  18114  evl1gsumdlem  18160  madugsum  18909  iunmbl2  21699  gsumvsca1  27433  gsumvsca2  27434  iblsplitf  31288  fsummsndifre  31814  fsumsplitsndif  31815  fsummmodsndifre  31816  fsummmodsnunz  31817