Metamath Proof Explorer

Theorem fneu2

Description: There is exactly one value of a function. (Contributed by NM, 7-Nov-1995)

Ref Expression
Assertion fneu2 
|- ( ( F Fn A /\ B e. A ) -> E! y <. B , y >. e. F )

Proof

Step Hyp Ref Expression
1 fneu 
 |-  ( ( F Fn A /\ B e. A ) -> E! y B F y )
2 df-br 
 |-  ( B F y <-> <. B , y >. e. F )
3 2 eubii 
 |-  ( E! y B F y <-> E! y <. B , y >. e. F )
4 1 3 sylib 
 |-  ( ( F Fn A /\ B e. A ) -> E! y <. B , y >. e. F )