Theorem raleqd

Description: Equality deduction for restricted universal quantifier. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	raleqd.a	⊢ Ⅎ 𝑥 𝐴
	raleqd.b	⊢ Ⅎ 𝑥 𝐵
	raleqd.e	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	raleqd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		raleqd.a	⊢ Ⅎ 𝑥 𝐴
2		raleqd.b	⊢ Ⅎ 𝑥 𝐵
3		raleqd.e	⊢ ( 𝜑 → 𝐴 = 𝐵 )
4	1 2	raleqf	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
5	3 4	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )