Theorem reuxfr1

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhyp to eliminate the second hypothesis. (Contributed by NM, 14-Nov-2004)

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

Proof

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