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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-aov | ||
2 | 1 | eleq1i | |
3 | afvvfunressn | ||
4 | 2 3 | sylbi |