Metamath Proof Explorer


Theorem funeu

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 FunFAFB∃!yAFy

Proof

Step Hyp Ref Expression
1 funrel FunFRelF
2 releldm RelFAFBAdomF
3 1 2 sylan FunFAFBAdomF
4 eldmg AdomFAdomFyAFy
5 4 ibi AdomFyAFy
6 3 5 syl FunFAFByAFy
7 funmo FunF*yAFy
8 7 adantr FunFAFB*yAFy
9 moeu *yAFyyAFy∃!yAFy
10 8 9 sylib FunFAFByAFy∃!yAFy
11 6 10 mpd FunFAFB∃!yAFy