Theorem rsp3eq

Description: From a restricted universal statement over A , specialize to an arbitrary element class, cf. rsp3 . (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	rsp3eq	|- ( A. x e. A ph -> ( ( y = B /\ B 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		eqeltr	|- ( ( y = B /\ B e. A ) -> y e. A )
7	1 2 3 4 5	rsp3	|- ( A. x e. A ph -> ( y e. A -> ps ) )
8	6 7	syl5	|- ( A. x e. A ph -> ( ( y = B /\ B e. A ) -> ps ) )