Metamath Proof Explorer

Theorem ndmovg

Description: The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008)

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

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
2 eleq2 
 |-  ( dom F = ( R X. S ) -> ( <. A , B >. e. dom F <-> <. A , B >. e. ( R X. S ) ) )
3 opelxp 
 |-  ( <. A , B >. e. ( R X. S ) <-> ( A e. R /\ B e. S ) )
4 2 3 bitrdi 
 |-  ( dom F = ( R X. S ) -> ( <. A , B >. e. dom F <-> ( A e. R /\ B e. S ) ) )
5 4 notbid 
 |-  ( dom F = ( R X. S ) -> ( -. <. A , B >. e. dom F <-> -. ( A e. R /\ B e. S ) ) )
6 ndmfv 
 |-  ( -. <. A , B >. e. dom F -> ( F ` <. A , B >. ) = (/) )
7 5 6 syl6bir 
 |-  ( dom F = ( R X. S ) -> ( -. ( A e. R /\ B e. S ) -> ( F ` <. A , B >. ) = (/) ) )
8 7 imp 
 |-  ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( F ` <. A , B >. ) = (/) )
9 1 8 eqtrid 
 |-  ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( A F B ) = (/) )