This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 = ( 𝑆 × 𝑆 )
Assertion ndmov ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ∅ )

Proof

Step Hyp Ref Expression
1 ndmov.1 ⊢ dom 𝐹 = ( 𝑆 × 𝑆 )
2 ndmovg ⊢ ( ( dom 𝐹 = ( 𝑆 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) ) → ( 𝐴 𝐹 𝐵 ) = ∅ )
3 1 2 mpan ⊢ ( ¬ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ( 𝐴 𝐹 𝐵 ) = ∅ )