Theorem rsp

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996)

	Ref	Expression
Assertion	rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) )
2		sp	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
3	1 2	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )