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 F = S \times S$
	Assertion	ndmov	$⊢ \neg (A \in S \land B \in S) \to A F B = \emptyset$

Step	Hyp	Ref	Expression
1		ndmov.1	$⊢ dom F = S \times S$
2		ndmovg	$⊢ (dom F = S \times S \land \neg (A \in S \land B \in S)) \to A F B = \emptyset$
3	1 2	mpan	$⊢ \neg (A \in S \land B \in S) \to A F B = \emptyset$