Theorem rspcsbela 3797

Description: Special case related to rspsbc 3348. (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 3348	. . 3 |- ( A e. B -> ( A. x e. B C e. D -> [. A / x ]. C e. D ) )
2		sbcel1g 3778	. . 3 |- ( A e. B -> ( [. A / x ]. C e. D <-> [_ A / x ]_ C e. D ) )
3	1, 2	sylibd 218	. 2 |- ( A e. B -> ( A. x e. B C e. D -> [_ A / x ]_ C e. D ) )
4	3	imp 431	1 |- ( ( A e. B /\ A. x e. B C e. D ) -> [_ A / x ]_ C e. D )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1889   A.wral 2739   [.wsbc 3269   [_csb 3365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-in 3413  df-ss 3420  df-nul 3734

This theorem is referenced by:  mptnn0fsupp  12216  mptnn0fsuppr  12218  fsumzcl2  13816  fsummsnunz  13827  fsumsplitsnun  13828  modfsummodslem1  13864  gsummpt1n0  17609  gsummptnn0fz  17627  telgsumfzslem  17630  telgsumfzs  17631  telgsums  17635  mptscmfsupp0  18165  coe1fzgsumdlem  18907  gsummoncoe1  18910  evl1gsumdlem  18956  madugsum  19680  iunmbl2  22522  gsumvsca1  28557  gsumvsca2  28558  esum2dlem  28925  esumiun  28927  iblsplitf  37857  fsummsndifre  39101  fsumsplitsndif  39102  fsummmodsndifre  39103  fsummmodsnunz  39104