Metamath Proof Explorer

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 
|- ( -. <. A , B >. e. dom F -> (( A F B )) = _V )

Proof

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