# Metamath Proof Explorer

## Theorem fovcl

Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007)

Ref Expression
Hypothesis fovcl.1 ${⊢}{F}:{R}×{S}⟶{C}$
Assertion fovcl ${⊢}\left({A}\in {R}\wedge {B}\in {S}\right)\to {A}{F}{B}\in {C}$

### Proof

Step Hyp Ref Expression
1 fovcl.1 ${⊢}{F}:{R}×{S}⟶{C}$
2 ffnov ${⊢}{F}:{R}×{S}⟶{C}↔\left({F}Fn\left({R}×{S}\right)\wedge \forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}\right)$
3 2 simprbi ${⊢}{F}:{R}×{S}⟶{C}\to \forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}$
4 1 3 ax-mp ${⊢}\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}$
5 oveq1 ${⊢}{x}={A}\to {x}{F}{y}={A}{F}{y}$
6 5 eleq1d ${⊢}{x}={A}\to \left({x}{F}{y}\in {C}↔{A}{F}{y}\in {C}\right)$
7 oveq2 ${⊢}{y}={B}\to {A}{F}{y}={A}{F}{B}$
8 7 eleq1d ${⊢}{y}={B}\to \left({A}{F}{y}\in {C}↔{A}{F}{B}\in {C}\right)$
9 6 8 rspc2v ${⊢}\left({A}\in {R}\wedge {B}\in {S}\right)\to \left(\forall {x}\in {R}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{F}{y}\in {C}\to {A}{F}{B}\in {C}\right)$
10 4 9 mpi ${⊢}\left({A}\in {R}\wedge {B}\in {S}\right)\to {A}{F}{B}\in {C}$