ndmaovg

Description: The value of an operation outside its domain, analogous to ndmovg . (Contributed by Alexander van der Vekens, 26-May-2017)

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

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨A, B⟩ \in (R \times S) \leftrightarrow (A \in R \land B \in S)$
2		eleq2	$⊢ R \times S = dom F \to (⟨A, B⟩ \in (R \times S) \leftrightarrow ⟨A, B⟩ \in dom F)$
3	2	eqcoms	$⊢ dom F = R \times S \to (⟨A, B⟩ \in (R \times S) \leftrightarrow ⟨A, B⟩ \in dom F)$
4	1 3	bitr3id	$⊢ dom F = R \times S \to ((A \in R \land B \in S) \leftrightarrow ⟨A, B⟩ \in dom F)$
5	4	notbid	$⊢ dom F = R \times S \to (\neg (A \in R \land B \in S) \leftrightarrow \neg ⟨A, B⟩ \in dom F)$
6	5	biimpa	$⊢ (dom F = R \times S \land \neg (A \in R \land B \in S)) \to \neg ⟨A, B⟩ \in dom F$
7		ndmaov	$⊢ \neg ⟨A, B⟩ \in dom F \to ((A F B)) = V$
8	6 7	syl	$⊢ (dom F = R \times S \land \neg (A \in R \land B \in S)) \to ((A F B)) = V$

Metamath Proof Explorer