Theorem raleqd

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

	Ref	Expression
Hypotheses	raleqd.a	$$⊢\underset{\_}{Ⅎ}xA$$
	raleqd.b	$$⊢\underset{\_}{Ⅎ}xB$$
	raleqd.e	$$⊢\phi \to A=B$$
Assertion	raleqd	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raleqd.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		raleqd.b	$$⊢\underset{\_}{Ⅎ}xB$$
3		raleqd.e	$$⊢\phi \to A=B$$
4	1 2	raleqf	$$⊢A=B\to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$
5	3 4	syl	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$