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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		rspsbc	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → [ 𝐴 / 𝑥 ] 𝐶 ∈ 𝐷 ) )
2		sbcel1g	⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝐶 ∈ 𝐷 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝐷 ) )
3	1 2	sylibd	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝐷 ) )
4	3	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝐶 ∈ 𝐷 ) → ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ∈ 𝐷 )