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	⊢ Ⅎ 𝑥 𝐴
	rsp3.2	⊢ Ⅎ 𝑦 𝐴
	rsp3.3	⊢ Ⅎ 𝑦 𝜑
	rsp3.4	⊢ Ⅎ 𝑥 𝜓
	rsp3.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	rsp3	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑦 ∈ 𝐴 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rsp3.1	⊢ Ⅎ 𝑥 𝐴
2		rsp3.2	⊢ Ⅎ 𝑦 𝐴
3		rsp3.3	⊢ Ⅎ 𝑦 𝜑
4		rsp3.4	⊢ Ⅎ 𝑥 𝜓
5		rsp3.5	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
6	1 2 3 4 5	cbvralfw	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 𝜓 )
7		rsp	⊢ ( ∀ 𝑦 ∈ 𝐴 𝜓 → ( 𝑦 ∈ 𝐴 → 𝜓 ) )
8	6 7	sylbi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 → ( 𝑦 ∈ 𝐴 → 𝜓 ) )