Theorem funmo

Description: A function has at most one value for each argument. (Contributed by NM, 24-May-1998) (Proof shortened by SN, 19-Dec-2024)

	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	1	simprbi	|- ( Fun F -> A. x E* y x F y )
9		breq1	|- ( x = A -> ( x F y <-> A F y ) )
10	9	mobidv	|- ( x = A -> ( E* y x F y <-> E* y A F y ) )
11	10	spcgv	|- ( A e. _V -> ( A. x E* y x F y -> E* y A F y ) )
12	8 11	syl5com	|- ( Fun F -> ( A e. _V -> E* y A F y ) )
13		moanimv	|- ( E* y ( A e. _V /\ A F y ) <-> ( A e. _V -> E* y A F y ) )
14	12 13	sylibr	|- ( Fun F -> E* y ( A e. _V /\ A F y ) )
15		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 ) )
16	7 14 15	sylc	|- ( Fun F -> E* y A F y )