This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rspa

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

		Ref	Expression
	Assertion	rspa	$⊢ (\forall x \in A φ \land x \in A) \to φ$

Step	Hyp	Ref	Expression
1		rsp	$⊢ \forall x \in A φ \to (x \in A \to φ)$
2	1	imp	$⊢ (\forall x \in A φ \land x \in A) \to φ$