Theorem rsp3

Description: From a restricted universal statement over A , specialize to an arbitrary element y e. A , cf. rsp . (Contributed by Peter Mazsa, 9-Feb-2026)

	Ref	Expression
Hypotheses	rsp3.1	$$⊢\underset{\_}{Ⅎ}xA$$
	rsp3.2	$$⊢\underset{\_}{Ⅎ}yA$$
	rsp3.3	$$⊢Ⅎy\phi$$
	rsp3.4	$$⊢Ⅎx\psi$$
	rsp3.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rsp3	$$⊢\forall x\in A\phi \to \left(y\in A\to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rsp3.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		rsp3.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		rsp3.3	$$⊢Ⅎy\phi$$
4		rsp3.4	$$⊢Ⅎx\psi$$
5		rsp3.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6	1 2 3 4 5	cbvralfw	$$⊢\forall x\in A\phi \leftrightarrow \forall y\in A\psi$$
7		rsp	$$⊢\forall y\in A\psi \to \left(y\in A\to \psi \right)$$
8	6 7	sylbi	$$⊢\forall x\in A\phi \to \left(y\in A\to \psi \right)$$