fneu

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	fneu	$⊢ (F Fn A \land B \in A) \to \exists! y B F y$

Step	Hyp	Ref	Expression
1		funmo	$⊢ Fun F \to \exists^{*} y B F y$
2	1	adantr	$⊢ (Fun F \land B \in dom F) \to \exists^{*} y B F y$
3		eldmg	$⊢ B \in dom F \to (B \in dom F \leftrightarrow \exists y B F y)$
4	3	ibi	$⊢ B \in dom F \to \exists y B F y$
5	4	adantl	$⊢ (Fun F \land B \in dom F) \to \exists y B F y$
6		exmoeub	$⊢ \exists y B F y \to (\exists^{*} y B F y \leftrightarrow \exists! y B F y)$
7	5 6	syl	$⊢ (Fun F \land B \in dom F) \to (\exists^{*} y B F y \leftrightarrow \exists! y B F y)$
8	2 7	mpbid	$⊢ (Fun F \land B \in dom F) \to \exists! y B F y$
9	8	funfni	$⊢ (F Fn A \land B \in A) \to \exists! y B F y$

Metamath Proof Explorer