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

Proof

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