This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funeu2

Description: There is exactly one value of a function. (Contributed by NM, 3-Aug-1994)

		Ref	Expression
	Assertion	funeu2	$⊢ (Fun F \land ⟨A, B⟩ \in F) \to \exists! y ⟨A, y⟩ \in F$

Step	Hyp	Ref	Expression
1		df-br	$⊢ A F B \leftrightarrow ⟨A, B⟩ \in F$
2		funeu	$⊢ (Fun F \land A F B) \to \exists! y A F y$
3		df-br	$⊢ A F y \leftrightarrow ⟨A, y⟩ \in F$
4	3	eubii	$⊢ \exists! y A F y \leftrightarrow \exists! y ⟨A, y⟩ \in F$
5	2 4	sylib	$⊢ (Fun F \land A F B) \to \exists! y ⟨A, y⟩ \in F$
6	1 5	sylan2br	$⊢ (Fun F \land ⟨A, B⟩ \in F) \to \exists! y ⟨A, y⟩ \in F$