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 ) = (/) )