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 )