Metamath Proof Explorer

Theorem nssdmovg

Description: The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017)

Ref Expression
Assertion nssdmovg 
|- ( ( dom F C_ ( 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 ssel2 
 |-  ( ( dom F C_ ( 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 sylib 
 |-  ( ( dom F C_ ( R X. S ) /\ <. A , B >. e. dom F ) -> ( A e. R /\ B e. S ) )
5 4 stoic1a 
 |-  ( ( dom F C_ ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> -. <. A , B >. e. dom F )
6 ndmfv 
 |-  ( -. <. A , B >. e. dom F -> ( F ` <. A , B >. ) = (/) )
7 5 6 syl 
 |-  ( ( dom F C_ ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( F ` <. A , B >. ) = (/) )
8 1 7 eqtrid 
 |-  ( ( dom F C_ ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> ( A F B ) = (/) )