Theorem rexeqbii

Description: Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	rexeqbii.1	$$⊢A=B$$
	rexeqbii.2	$$⊢\psi \leftrightarrow \chi$$
Assertion	rexeqbii	$$⊢\exists x\in A\psi \leftrightarrow \exists x\in B\chi$$

Proof

Step	Hyp	Ref	Expression
1		rexeqbii.1	$$⊢A=B$$
2		rexeqbii.2	$$⊢\psi \leftrightarrow \chi$$
3	1	eleq2i	$$⊢x\in A\leftrightarrow x\in B$$
4	3 2	anbi12i	$$⊢\left(x\in A\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \chi \right)$$
5	4	rexbii2	$$⊢\exists x\in A\psi \leftrightarrow \exists x\in B\chi$$