# Metamath Proof Explorer

## 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}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}$

### Proof

Step Hyp Ref Expression
1 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
2 fneu2 ${⊢}\left({F}Fn{A}\wedge {C}\in {A}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}$
3 1 2 sylan ${⊢}\left({F}:{A}⟶{B}\wedge {C}\in {A}\right)\to \exists !{y}\phantom{\rule{.4em}{0ex}}⟨{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}↔\left({y}\in {B}\wedge ⟨{C},{y}⟩\in {F}\right)\right)$
8 7 eubidv ${⊢}{F}:{A}⟶{B}\to \left(\exists !{y}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\wedge ⟨{C},{y}⟩\in {F}\right)$
11 df-reu ${⊢}\exists !{y}\in {B}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}↔\exists !{y}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}⟨{C},{y}⟩\in {F}$