Theorem reuxfr

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . (Contributed by NM, 14-Nov-2004) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Hypotheses	reuxfr.1	$$⊢y\in C\to A\in B$$
	reuxfr.2	$$⊢x\in B\to {\exists }^{*}y\in Cx=A$$
Assertion	reuxfr	$$⊢\exists !x\in B\exists y\in C\left(x=A\wedge \phi \right)\leftrightarrow \exists !y\in C\phi$$

Proof

Step	Hyp	Ref	Expression
1		reuxfr.1	$$⊢y\in C\to A\in B$$
2		reuxfr.2	$$⊢x\in B\to {\exists }^{*}y\in Cx=A$$
3	1	adantl	$$⊢\left(\top \wedge y\in C\right)\to A\in B$$
4	2	adantl	$$⊢\left(\top \wedge x\in B\right)\to {\exists }^{*}y\in Cx=A$$
5	3 4	reuxfrd	$$⊢\top \to \left(\exists !x\in B\exists y\in C\left(x=A\wedge \phi \right)\leftrightarrow \exists !y\in C\phi \right)$$
6	5	mptru	$$⊢\exists !x\in B\exists y\in C\left(x=A\wedge \phi \right)\leftrightarrow \exists !y\in C\phi$$