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	|- F/_ x A
	rsp3.2	|- F/_ y A
	rsp3.3	|- F/ y ph
	rsp3.4	|- F/ x ps
	rsp3.5	|- ( x = y -> ( ph <-> ps ) )
Assertion	rsp3	|- ( A. x e. A ph -> ( y e. A -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rsp3.1	|- F/_ x A
2		rsp3.2	|- F/_ y A
3		rsp3.3	|- F/ y ph
4		rsp3.4	|- F/ x ps
5		rsp3.5	|- ( x = y -> ( ph <-> ps ) )
6	1 2 3 4 5	cbvralfw	|- ( A. x e. A ph <-> A. y e. A ps )
7		rsp	|- ( A. y e. A ps -> ( y e. A -> ps ) )
8	6 7	sylbi	|- ( A. x e. A ph -> ( y e. A -> ps ) )