Theorem raleqi

Description: Equality inference for restricted universal quantifier. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Hypothesis	raleq1i.1	$$⊢A=B$$
Assertion	raleqi	$$⊢\forall x\in A\phi \leftrightarrow \forall x\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		raleq1i.1	$$⊢A=B$$
2		raleq	$$⊢A=B\to \left(\forall x\in A\phi \leftrightarrow \forall x\in B\phi \right)$$
3	1 2	ax-mp	$$⊢\forall x\in A\phi \leftrightarrow \forall x\in B\phi$$