Theorem fneu2

Description: There is exactly one value of a function. (Contributed by NM, 7-Nov-1995)

	Ref	Expression
Assertion	fneu2	$$⊢\left(FFnA\wedge B\in A\right)\to \exists !y⟨B,y⟩\in F$$

Proof

Step	Hyp	Ref	Expression
1		fneu	$$⊢\left(FFnA\wedge B\in A\right)\to \exists !yBFy$$
2		df-br	$$⊢BFy\leftrightarrow ⟨B,y⟩\in F$$
3	2	eubii	$$⊢\exists !yBFy\leftrightarrow \exists !y⟨B,y⟩\in F$$
4	1 3	sylib	$$⊢\left(FFnA\wedge B\in A\right)\to \exists !y⟨B,y⟩\in F$$