Description: There is exactly one value of a function. (Contributed by NM, 22-Apr-2004) (Proof shortened by Andrew Salmon, 17-Sep-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | funeu | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funrel | |
|
2 | releldm | |
|
3 | 1 2 | sylan | |
4 | eldmg | |
|
5 | 4 | ibi | |
6 | 3 5 | syl | |
7 | funmo | |
|
8 | 7 | adantr | |
9 | moeu | |
|
10 | 8 9 | sylib | |
11 | 6 10 | mpd | |