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 )