funeu

Description: There is exactly one value of a function. (Contributed by NM, 22-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Assertion	funeu	$⊢ (Fun F \land A F B) \to \exists! y A F y$

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		releldm	$⊢ (Rel F \land A F B) \to A \in dom F$
3	1 2	sylan	$⊢ (Fun F \land A F B) \to A \in dom F$
4		eldmg	$⊢ A \in dom F \to (A \in dom F \leftrightarrow \exists y A F y)$
5	4	ibi	$⊢ A \in dom F \to \exists y A F y$
6	3 5	syl	$⊢ (Fun F \land A F B) \to \exists y A F y$
7		funmo	$⊢ Fun F \to \exists^{*} y A F y$
8	7	adantr	$⊢ (Fun F \land A F B) \to \exists^{*} y A F y$
9		moeu	$⊢ \exists^{*} y A F y \leftrightarrow (\exists y A F y \to \exists! y A F y)$
10	8 9	sylib	$⊢ (Fun F \land A F B) \to (\exists y A F y \to \exists! y A F y)$
11	6 10	mpd	$⊢ (Fun F \land A F B) \to \exists! y A F y$

Metamath Proof Explorer