Metamath Proof Explorer

Theorem ndmov

Description: The value of an operation outside its domain. (Contributed by NM, 24-Aug-1995)

Ref Expression
Hypothesis ndmov.1 
|- dom F = ( S X. S )
Assertion ndmov 
|- ( -. ( A e. S /\ B e. S ) -> ( A F B ) = (/) )

Proof

Step Hyp Ref Expression
1 ndmov.1 
 |-  dom F = ( S X. S )
2 ndmovg 
 |-  ( ( dom F = ( S X. S ) /\ -. ( A e. S /\ B e. S ) ) -> ( A F B ) = (/) )
3 1 2 mpan 
 |-  ( -. ( A e. S /\ B e. S ) -> ( A F B ) = (/) )