Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998)

	Ref	Expression
Assertion	funmo	|- ( Fun F -> E* y A F y )

Proof

Step	Hyp	Ref	Expression
1		dffun6	|- ( Fun F <-> ( Rel F /\ A. x E* y x F y ) )
2	1	simplbi	|- ( Fun F -> Rel F )
3		brrelex1	|- ( ( Rel F /\ A F y ) -> A e. _V )
4	3	ex	|- ( Rel F -> ( A F y -> A e. _V ) )
5	2 4	syl	|- ( Fun F -> ( A F y -> A e. _V ) )
6	5	ancrd	|- ( Fun F -> ( A F y -> ( A e. _V /\ A F y ) ) )
7	6	alrimiv	|- ( Fun F -> A. y ( A F y -> ( A e. _V /\ A F y ) ) )
8		breq1	|- ( x = A -> ( x F y <-> A F y ) )
9	8	mobidv	|- ( x = A -> ( E* y x F y <-> E* y A F y ) )
10	9	imbi2d	|- ( x = A -> ( ( Fun F -> E* y x F y ) <-> ( Fun F -> E* y A F y ) ) )
11	1	simprbi	|- ( Fun F -> A. x E* y x F y )
12	11	19.21bi	|- ( Fun F -> E* y x F y )
13	10 12	vtoclg	|- ( A e. _V -> ( Fun F -> E* y A F y ) )
14	13	com12	|- ( Fun F -> ( A e. _V -> E* y A F y ) )
15		moanimv	|- ( E* y ( A e. _V /\ A F y ) <-> ( A e. _V -> E* y A F y ) )
16	14 15	sylibr	|- ( Fun F -> E* y ( A e. _V /\ A F y ) )
17		moim	|- ( A. y ( A F y -> ( A e. _V /\ A F y ) ) -> ( E* y ( A e. _V /\ A F y ) -> E* y A F y ) )
18	7 16 17	sylc	|- ( Fun F -> E* y A F y )