Theorem rexeqbid

Description: Equality deduction for restricted existential quantifier. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypotheses	raleqbid.0	$$⊢Ⅎx\phi$$
	raleqbid.1	$$⊢\underset{\_}{Ⅎ}xA$$
	raleqbid.2	$$⊢\underset{\_}{Ⅎ}xB$$
	raleqbid.3	$$⊢\phi \to A=B$$
	raleqbid.4	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	rexeqbid	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists x\in B\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raleqbid.0	$$⊢Ⅎx\phi$$
2		raleqbid.1	$$⊢\underset{\_}{Ⅎ}xA$$
3		raleqbid.2	$$⊢\underset{\_}{Ⅎ}xB$$
4		raleqbid.3	$$⊢\phi \to A=B$$
5		raleqbid.4	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
6	2 3	rexeqf	$$⊢A=B\to \left(\exists x\in A\psi \leftrightarrow \exists x\in B\psi \right)$$
7	4 6	syl	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists x\in B\psi \right)$$
8	1 5	rexbid	$$⊢\phi \to \left(\exists x\in B\psi \leftrightarrow \exists x\in B\chi \right)$$
9	7 8	bitrd	$$⊢\phi \to \left(\exists x\in A\psi \leftrightarrow \exists x\in B\chi \right)$$