ndmovg

Description: The value of an operation outside its domain. (Contributed by NM, 28-Mar-2008)

		Ref	Expression
	Assertion	ndmovg	$⊢ (dom F = R \times S \land \neg (A \in R \land B \in S)) \to A F B = \emptyset$

Step	Hyp	Ref	Expression
1		df-ov	$⊢ A F B = F (⟨A, B⟩)$
2		eleq2	$⊢ dom F = R \times S \to (⟨A, B⟩ \in dom F \leftrightarrow ⟨A, B⟩ \in (R \times S))$
3		opelxp	$⊢ ⟨A, B⟩ \in (R \times S) \leftrightarrow (A \in R \land B \in S)$
4	2 3	bitrdi	$⊢ dom F = R \times S \to (⟨A, B⟩ \in dom F \leftrightarrow (A \in R \land B \in S))$
5	4	notbid	$⊢ dom F = R \times S \to (\neg ⟨A, B⟩ \in dom F \leftrightarrow \neg (A \in R \land B \in S))$
6		ndmfv	$⊢ \neg ⟨A, B⟩ \in dom F \to F (⟨A, B⟩) = \emptyset$
7	5 6	biimtrrdi	$⊢ dom F = R \times S \to (\neg (A \in R \land B \in S) \to F (⟨A, B⟩) = \emptyset)$
8	7	imp	$⊢ (dom F = R \times S \land \neg (A \in R \land B \in S)) \to F (⟨A, B⟩) = \emptyset$
9	1 8	eqtrid	$⊢ (dom F = R \times S \land \neg (A \in R \land B \in S)) \to A F B = \emptyset$

Metamath Proof Explorer