# Metamath Proof Explorer

## Theorem ovprc

Description: The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypothesis ovprc1.1 ${⊢}\mathrm{Rel}\mathrm{dom}{F}$
Assertion ovprc ${⊢}¬\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to {A}{F}{B}=\varnothing$

### Proof

Step Hyp Ref Expression
1 ovprc1.1 ${⊢}\mathrm{Rel}\mathrm{dom}{F}$
2 df-ov ${⊢}{A}{F}{B}={F}\left(⟨{A},{B}⟩\right)$
3 df-br ${⊢}{A}\mathrm{dom}{F}{B}↔⟨{A},{B}⟩\in \mathrm{dom}{F}$
4 1 brrelex12i ${⊢}{A}\mathrm{dom}{F}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
5 3 4 sylbir ${⊢}⟨{A},{B}⟩\in \mathrm{dom}{F}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
6 ndmfv ${⊢}¬⟨{A},{B}⟩\in \mathrm{dom}{F}\to {F}\left(⟨{A},{B}⟩\right)=\varnothing$
7 5 6 nsyl5 ${⊢}¬\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to {F}\left(⟨{A},{B}⟩\right)=\varnothing$
8 2 7 syl5eq ${⊢}¬\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to {A}{F}{B}=\varnothing$