Metamath Proof Explorer

Theorem rspcsbela

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

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

Proof

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