Theorem raleqdv

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005)

	Ref	Expression
Hypothesis	raleqdv.1	$$⊢\phi \to A=B$$
Assertion	raleqdv	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raleqdv.1	$$⊢\phi \to A=B$$
2		raleq	$$⊢A=B\to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$
3	1 2	syl	$$⊢\phi \to \left(\forall x\in A\psi \leftrightarrow \forall x\in B\psi \right)$$