Theorem aovnfundmuv

Description: If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	aovnfundmuv	|- ( -. F defAt <. A , B >. -> (( A F B )) = _V )

Proof

Step	Hyp	Ref	Expression
1		df-aov	|- (( A F B )) = ( F ''' <. A , B >. )
2		afvnfundmuv	|- ( -. F defAt <. A , B >. -> ( F ''' <. A , B >. ) = _V )
3	1 2	syl5eq	|- ( -. F defAt <. A , B >. -> (( A F B )) = _V )