Theorem rspw

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

	Ref	Expression
Hypothesis	rspw.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rspw	$$⊢\forall x\in A\phi \to \left(x\in A\to \phi \right)$$

Proof

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