Theorem reuhyp

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 . (Contributed by NM, 15-Nov-2004)

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

Proof

Step	Hyp	Ref	Expression
1		reuhyp.1	$$⊢x\in C\to B\in C$$
2		reuhyp.2	$$⊢\left(x\in C\wedge y\in C\right)\to \left(x=A\leftrightarrow y=B\right)$$
3		tru	$$⊢\top$$
4	1	adantl	$$⊢\left(\top \wedge x\in C\right)\to B\in C$$
5	2	3adant1	$$⊢\left(\top \wedge x\in C\wedge y\in C\right)\to \left(x=A\leftrightarrow y=B\right)$$
6	4 5	reuhypd	$$⊢\left(\top \wedge x\in C\right)\to \exists !y\in Cx=A$$
7	3 6	mpan	$$⊢x\in C\to \exists !y\in Cx=A$$