Theorem funeu2

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

	Ref	Expression
Assertion	funeu2	$$⊢\left(\mathrm{Fun}F\wedge ⟨A,B⟩\in F\right)\to \exists !y⟨A,y⟩\in F$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢AFB\leftrightarrow ⟨A,B⟩\in F$$
2		funeu	$$⊢\left(\mathrm{Fun}F\wedge AFB\right)\to \exists !yAFy$$
3		df-br	$$⊢AFy\leftrightarrow ⟨A,y⟩\in F$$
4	3	eubii	$$⊢\exists !yAFy\leftrightarrow \exists !y⟨A,y⟩\in F$$
5	2 4	sylib	$$⊢\left(\mathrm{Fun}F\wedge AFB\right)\to \exists !y⟨A,y⟩\in F$$
6	1 5	sylan2br	$$⊢\left(\mathrm{Fun}F\wedge ⟨A,B⟩\in F\right)\to \exists !y⟨A,y⟩\in F$$