Theorem rspa

Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜑 ) )
2	1	imp	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝜑 )