Theorem rspcsbela 4006

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   A.wral 2912   [.wsbc 3435   [_csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-nul 3916

This theorem is referenced by:  el2mpt2csbcl  7250  mptnn0fsupp  12797  mptnn0fsuppr  12799  fsumzcl2  14469  fsummsnunz  14483  fsumsplitsnun  14484  fsummsnunzOLD  14485  fsumsplitsnunOLD  14486  modfsummodslem1  14524  fprodmodd  14728  sumeven  15110  sumodd  15111  gsummpt1n0  18364  gsummptnn0fz  18382  telgsumfzslem  18385  telgsumfzs  18386  telgsums  18390  mptscmfsupp0  18928  coe1fzgsumdlem  19671  gsummoncoe1  19674  evl1gsumdlem  19720  madugsum  20449  iunmbl2  23325  gsumvsca1  29782  gsumvsca2  29783  esum2dlem  30154  esumiun  30156  iblsplitf  40186  fsummsndifre  41342  fsumsplitsndif  41343  fsummmodsndifre  41344  fsummmodsnunz  41345