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	$$⊢\left(A\in B\wedge \forall x\in BC\in D\right)\to ⦋A/x⦌C\in D$$

Proof

Step	Hyp	Ref	Expression
1		rspsbc	$$⊢A\in B\to \left(\forall x\in BC\in D\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\in D\right)$$
2		sbcel1g	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}C\in D\leftrightarrow ⦋A/x⦌C\in D\right)$$
3	1 2	sylibd	$$⊢A\in B\to \left(\forall x\in BC\in D\to ⦋A/x⦌C\in D\right)$$
4	3	imp	$$⊢\left(A\in B\wedge \forall x\in BC\in D\right)\to ⦋A/x⦌C\in D$$