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 ∈ B ∧ ∀ x ∈ B C ∈ D → ⦋ A / x⦌ C ∈ D

Proof

Step Hyp Ref Expression
1 rspsbc ⊢ A ∈ B → ∀ x ∈ B C ∈ D → [˙A / x]˙ C ∈ D
2 sbcel1g ⊢ A ∈ B → [˙A / x]˙ C ∈ D ↔ ⦋ A / x⦌ C ∈ D
3 1 2 sylibd ⊢ A ∈ B → ∀ x ∈ B C ∈ D → ⦋ A / x⦌ C ∈ D
4 3 imp ⊢ A ∈ B ∧ ∀ x ∈ B C ∈ D → ⦋ A / x⦌ C ∈ D