# Metamath Proof Explorer

## Theorem ndmovg

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

Ref Expression
Assertion ndmovg ${⊢}\left(\mathrm{dom}{F}={R}×{S}\wedge ¬\left({A}\in {R}\wedge {B}\in {S}\right)\right)\to {A}{F}{B}=\varnothing$

### Proof

Step Hyp Ref Expression
1 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
2 eleq2 ${⊢}\mathrm{dom}{F}={R}×{S}\to \left(⟨{A},{B}⟩\in \mathrm{dom}{F}↔⟨{A},{B}⟩\in \left({R}×{S}\right)\right)$
3 opelxp ${⊢}⟨{A},{B}⟩\in \left({R}×{S}\right)↔\left({A}\in {R}\wedge {B}\in {S}\right)$
4 2 3 syl6bb ${⊢}\mathrm{dom}{F}={R}×{S}\to \left(⟨{A},{B}⟩\in \mathrm{dom}{F}↔\left({A}\in {R}\wedge {B}\in {S}\right)\right)$
5 4 notbid ${⊢}\mathrm{dom}{F}={R}×{S}\to \left(¬⟨{A},{B}⟩\in \mathrm{dom}{F}↔¬\left({A}\in {R}\wedge {B}\in {S}\right)\right)$
6 ndmfv ${⊢}¬⟨{A},{B}⟩\in \mathrm{dom}{F}\to {F}\left(⟨{A},{B}⟩\right)=\varnothing$
7 5 6 syl6bir ${⊢}\mathrm{dom}{F}={R}×{S}\to \left(¬\left({A}\in {R}\wedge {B}\in {S}\right)\to {F}\left(⟨{A},{B}⟩\right)=\varnothing \right)$
8 7 imp ${⊢}\left(\mathrm{dom}{F}={R}×{S}\wedge ¬\left({A}\in {R}\wedge {B}\in {S}\right)\right)\to {F}\left(⟨{A},{B}⟩\right)=\varnothing$
9 1 8 syl5eq ${⊢}\left(\mathrm{dom}{F}={R}×{S}\wedge ¬\left({A}\in {R}\wedge {B}\in {S}\right)\right)\to {A}{F}{B}=\varnothing$