Theorem feu

Description: There is exactly one value of a function in its codomain. (Contributed by NM, 10-Dec-2003)

	Ref	Expression
Assertion	feu	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \exists !y\in B⟨C,y⟩\in F$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:A⟶B\to FFnA$$
2		fneu2	$$⊢\left(FFnA\wedge C\in A\right)\to \exists !y⟨C,y⟩\in F$$
3	1 2	sylan	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \exists !y⟨C,y⟩\in F$$
4		opelf	$$⊢\left(F:A⟶B\wedge ⟨C,y⟩\in F\right)\to \left(C\in A\wedge y\in B\right)$$
5	4	simprd	$$⊢\left(F:A⟶B\wedge ⟨C,y⟩\in F\right)\to y\in B$$
6	5	ex	$$⊢F:A⟶B\to \left(⟨C,y⟩\in F\to y\in B\right)$$
7	6	pm4.71rd	$$⊢F:A⟶B\to \left(⟨C,y⟩\in F\leftrightarrow \left(y\in B\wedge ⟨C,y⟩\in F\right)\right)$$
8	7	eubidv	$$⊢F:A⟶B\to \left(\exists !y⟨C,y⟩\in F\leftrightarrow \exists !y\left(y\in B\wedge ⟨C,y⟩\in F\right)\right)$$
9	8	adantr	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(\exists !y⟨C,y⟩\in F\leftrightarrow \exists !y\left(y\in B\wedge ⟨C,y⟩\in F\right)\right)$$
10	3 9	mpbid	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \exists !y\left(y\in B\wedge ⟨C,y⟩\in F\right)$$
11		df-reu	$$⊢\exists !y\in B⟨C,y⟩\in F\leftrightarrow \exists !y\left(y\in B\wedge ⟨C,y⟩\in F\right)$$
12	10 11	sylibr	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \exists !y\in B⟨C,y⟩\in F$$