Metamath Proof Explorer


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 * y A F y

Proof

Step Hyp Ref Expression
1 dffun6 Fun F Rel F x * y x F y
2 1 simplbi Fun F Rel F
3 brrelex1 Rel F A F y A V
4 3 ex Rel F A F y A V
5 2 4 syl Fun F A F y A V
6 5 ancrd Fun F A F y A V A F y
7 6 alrimiv Fun F y A F y A V A F y
8 1 simprbi Fun F x * y x F y
9 breq1 x = A x F y A F y
10 9 mobidv x = A * y x F y * y A F y
11 10 spcgv A V x * y x F y * y A F y
12 8 11 syl5com Fun F A V * y A F y
13 moanimv * y A V A F y A V * y A F y
14 12 13 sylibr Fun F * y A V A F y
15 moim y A F y A V A F y * y A V A F y * y A F y
16 7 14 15 sylc Fun F * y A F y