This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( Fun F /\ A F B ) -> E! y A F y )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun F -> Rel F )
2 releldm 
 |-  ( ( Rel F /\ A F B ) -> A e. dom F )
3 1 2 sylan 
 |-  ( ( Fun F /\ A F B ) -> A e. dom F )
4 eldmg 
 |-  ( A e. dom F -> ( A e. dom F <-> E. y A F y ) )
5 4 ibi 
 |-  ( A e. dom F -> E. y A F y )
6 3 5 syl 
 |-  ( ( Fun F /\ A F B ) -> E. y A F y )
7 funmo 
 |-  ( Fun F -> E* y A F y )
8 7 adantr 
 |-  ( ( Fun F /\ A F B ) -> E* y A F y )
9 moeu 
 |-  ( E* y A F y <-> ( E. y A F y -> E! y A F y ) )
10 8 9 sylib 
 |-  ( ( Fun F /\ A F B ) -> ( E. y A F y -> E! y A F y ) )
11 6 10 mpd 
 |-  ( ( Fun F /\ A F B ) -> E! y A F y )