Theorem rexeqbi1dvOLD

Description: Obsolete version of rexeqbi1dv as of 5-May-2023. Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		raleqd.1	$$⊢A=B\to \left(\phi \leftrightarrow \psi \right)$$
2		rexeq	$$⊢A=B\to \left(\exists x\in A\phi \leftrightarrow \exists x\in B\phi \right)$$
3	1	rexbidv	$$⊢A=B\to \left(\exists x\in B\phi \leftrightarrow \exists x\in B\psi \right)$$
4	2 3	bitrd	$$⊢A=B\to \left(\exists x\in A\phi \leftrightarrow \exists x\in B\psi \right)$$