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	$$⊢\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	rsp3eq	$$⊢\forall x\in A\phi \to \left(\left(y=B\wedge B\in A\right)\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		eqeltr	$$⊢\left(y=B\wedge B\in A\right)\to y\in A$$
7	1 2 3 4 5	rsp3	$$⊢\forall x\in A\phi \to \left(y\in A\to \psi \right)$$
8	6 7	syl5	$$⊢\forall x\in A\phi \to \left(\left(y=B\wedge B\in A\right)\to \psi \right)$$