Theorem ndmaov

Description: The value of an operation outside its domain, analogous to ndmafv . (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Assertion	ndmaov	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) = V )

Proof

Step	Hyp	Ref	Expression
1		df-aov	⊢ (( 𝐴 𝐹 𝐵 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ )
2		ndmafv	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → ( 𝐹 ''' ⟨ 𝐴 , 𝐵 ⟩ ) = V )
3	1 2	syl5eq	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) = V )