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

Metamath Proof Explorer

Theorem fneu

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 fneu 
|- ( ( F Fn A /\ B e. A ) -> E! y B F y )

Proof

Step Hyp Ref Expression
1 funmo 
 |-  ( Fun F -> E* y B F y )
2 1 adantr 
 |-  ( ( Fun F /\ B e. dom F ) -> E* y B F y )
3 eldmg 
 |-  ( B e. dom F -> ( B e. dom F <-> E. y B F y ) )
4 3 ibi 
 |-  ( B e. dom F -> E. y B F y )
5 4 adantl 
 |-  ( ( Fun F /\ B e. dom F ) -> E. y B F y )
6 exmoeub 
 |-  ( E. y B F y -> ( E* y B F y <-> E! y B F y ) )
7 5 6 syl 
 |-  ( ( Fun F /\ B e. dom F ) -> ( E* y B F y <-> E! y B F y ) )
8 2 7 mpbid 
 |-  ( ( Fun F /\ B e. dom F ) -> E! y B F y )
9 8 funfni 
 |-  ( ( F Fn A /\ B e. A ) -> E! y B F y )