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	⊢ ( ¬ 𝐹 defAt ⟨ 𝐴 , 𝐵 ⟩ → (( 𝐴 𝐹 𝐵 )) = V )

Proof

Step	Hyp	Ref	Expression
1		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
2		afvnfundmuv	⊢ ( ¬ 𝐹 defAt ⟨ 𝐴 , 𝐵 ⟩ → ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V )
3	1 2	eqtrid	⊢ ( ¬ 𝐹 defAt ⟨ 𝐴 , 𝐵 ⟩ → (( 𝐴 𝐹 𝐵 )) = V )