Metamath Proof Explorer

Theorem ndmaovg

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

Ref Expression
Assertion ndmaovg 
|- ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> (( A F B )) = _V )

Proof

Step Hyp Ref Expression
1 opelxp 
 |-  ( <. A , B >. e. ( R X. S ) <-> ( A e. R /\ B e. S ) )
2 eleq2 
 |-  ( ( R X. S ) = dom F -> ( <. A , B >. e. ( R X. S ) <-> <. A , B >. e. dom F ) )
3 2 eqcoms 
 |-  ( dom F = ( R X. S ) -> ( <. A , B >. e. ( R X. S ) <-> <. A , B >. e. dom F ) )
4 1 3 bitr3id 
 |-  ( dom F = ( R X. S ) -> ( ( A e. R /\ B e. S ) <-> <. A , B >. e. dom F ) )
5 4 notbid 
 |-  ( dom F = ( R X. S ) -> ( -. ( A e. R /\ B e. S ) <-> -. <. A , B >. e. dom F ) )
6 5 biimpa 
 |-  ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> -. <. A , B >. e. dom F )
7 ndmaov 
 |-  ( -. <. A , B >. e. dom F -> (( A F B )) = _V )
8 6 7 syl 
 |-  ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> (( A F B )) = _V )