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 )