Metamath Proof Explorer

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	$⊢ (x \in C \land y \in C) \to (x = A \leftrightarrow y = B)$
Assertion	reuhyp	$⊢ x \in C \to \exists! y \in C x = A$

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