Metamath Proof Explorer


Theorem aovvfunressn

Description: If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion aovvfunressn A F B C Fun F A B

Proof

Step Hyp Ref Expression
1 df-aov A F B = F ''' A B
2 1 eleq1i A F B C F ''' A B C
3 afvvfunressn F ''' A B C Fun F A B
4 2 3 sylbi A F B C Fun F A B