Theorem 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 𝐹 = ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → (( 𝐴 𝐹 𝐵 )) = V )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ↔ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) )
2		eleq2	⊢ ( ( 𝑅 × 𝑆 ) = dom 𝐹 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) )
3	2	eqcoms	⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 × 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) )
4	1 3	bitr3id	⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) )
5	4	notbid	⊢ ( dom 𝐹 = ( 𝑅 × 𝑆 ) → ( ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 ) )
6	5	biimpa	⊢ ( ( dom 𝐹 = ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 )
7		ndmaov	⊢ ( ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ dom 𝐹 → (( 𝐴 𝐹 𝐵 )) = V )
8	6 7	syl	⊢ ( ( dom 𝐹 = ( 𝑅 × 𝑆 ) ∧ ¬ ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ) → (( 𝐴 𝐹 𝐵 )) = V )