# Metamath Proof Explorer

## Theorem ffnov

Description: An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004)

Ref Expression
Assertion ffnov ${⊢}{F}:{A}×{B}⟶{C}↔\left({F}Fn\left({A}×{B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}\right)$

### Proof

Step Hyp Ref Expression
1 ffnfv ${⊢}{F}:{A}×{B}⟶{C}↔\left({F}Fn\left({A}×{B}\right)\wedge \forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\in {C}\right)$
2 fveq2 ${⊢}{w}=⟨{x},{y}⟩\to {F}\left({w}\right)={F}\left(⟨{x},{y}⟩\right)$
3 df-ov ${⊢}{x}{F}{y}={F}\left(⟨{x},{y}⟩\right)$
4 2 3 syl6eqr ${⊢}{w}=⟨{x},{y}⟩\to {F}\left({w}\right)={x}{F}{y}$
5 4 eleq1d ${⊢}{w}=⟨{x},{y}⟩\to \left({F}\left({w}\right)\in {C}↔{x}{F}{y}\in {C}\right)$
6 5 ralxp ${⊢}\forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\in {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}$
7 6 anbi2i ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge \forall {w}\in \left({A}×{B}\right)\phantom{\rule{.4em}{0ex}}{F}\left({w}\right)\in {C}\right)↔\left({F}Fn\left({A}×{B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}\right)$
8 1 7 bitri ${⊢}{F}:{A}×{B}⟶{C}↔\left({F}Fn\left({A}×{B}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}\right)$