Theorem reueqd

Description: Equality deduction for restricted unique existential quantifier. (Contributed by NM, 5-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		rmoeqd.1	$$⊢A=B\to \left(\phi \leftrightarrow \psi \right)$$
2		reueq1	$$⊢A=B\to \left(\exists !x\in A\phi \leftrightarrow \exists !x\in B\phi \right)$$
3	1	reubidv	$$⊢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)$$