Metamath Proof Explorer


Theorem nfunsnaov

Description: If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion nfunsnaov ¬ Fun F A B A F B = V

Proof

Step Hyp Ref Expression
1 df-aov A F B = F ''' A B
2 nfunsnafv ¬ Fun F A B F ''' A B = V
3 1 2 syl5eq ¬ Fun F A B A F B = V