Theorem reuxfr1ds

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhypd to eliminate the second hypothesis. (Contributed by NM, 16-Jan-2012)

	Ref	Expression
Hypotheses	reuxfr1ds.1	$$⊢\left(\phi \wedge y\in C\right)\to A\in B$$
	reuxfr1ds.2	$$⊢\left(\phi \wedge x\in B\right)\to \exists !y\in Cx=A$$
	reuxfr1ds.3	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	reuxfr1ds	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		reuxfr1ds.1	$$⊢\left(\phi \wedge y\in C\right)\to A\in B$$
2		reuxfr1ds.2	$$⊢\left(\phi \wedge x\in B\right)\to \exists !y\in Cx=A$$
3		reuxfr1ds.3	$$⊢x=A\to \left(\psi \leftrightarrow \chi \right)$$
4	3	adantl	$$⊢\left(\phi \wedge x=A\right)\to \left(\psi \leftrightarrow \chi \right)$$
5	1 2 4	reuxfr1d	$$⊢\phi \to \left(\exists !x\in B\psi \leftrightarrow \exists !y\in C\chi \right)$$