Metamath Proof Explorer


Theorem funressnmo

Description: A function restricted to a singleton has at most one value for the singleton element as argument. (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion funressnmo A V Fun F A * y A F y

Proof

Step Hyp Ref Expression
1 sneq x = A x = A
2 1 reseq2d x = A F x = F A
3 2 funeqd x = A Fun F x Fun F A
4 breq1 x = A x F y A F y
5 4 mobidv x = A * y x F y * y A F y
6 3 5 imbi12d x = A Fun F x * y x F y Fun F A * y A F y
7 funressnvmo Fun F x * y x F y
8 6 7 vtoclg A V Fun F A * y A F y
9 8 imp A V Fun F A * y A F y