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

Metamath Proof Explorer

Theorem rspw

Description: Restricted specialization. Weak version of rsp , requiring ax-8 , but not ax-12 . (Contributed by GG, 3-Oct-2024)

		Ref	Expression
	Hypothesis	rspw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	rspw	$⊢ \forall x \in A φ \to (x \in A \to φ)$

Step	Hyp	Ref	Expression
1		rspw.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
3		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
4	3 1	imbi12d	$⊢ x = y \to ((x \in A \to φ) \leftrightarrow (y \in A \to ψ))$
5	4	spw	$⊢ \forall x (x \in A \to φ) \to (x \in A \to φ)$
6	2 5	sylbi	$⊢ \forall x \in A φ \to (x \in A \to φ)$