Theorem funeu2

Description: There is exactly one value of a function. (Contributed by NM, 3-Aug-1994)

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

Proof

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