Theorem rexeqi

Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015)

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

Proof

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