# Metamath Proof Explorer

## Theorem eqfnov2

Description: Two operators with the same domain are equal iff their values at each point in the domain are equal. (Contributed by Jeff Madsen, 7-Jun-2010)

Ref Expression
Assertion eqfnov2 ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {G}Fn\left({A}×{B}\right)\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)$

### Proof

Step Hyp Ref Expression
1 eqfnov ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {G}Fn\left({A}×{B}\right)\right)\to \left({F}={G}↔\left({A}×{B}={A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)\right)$
2 simpr ${⊢}\left({A}×{B}={A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}$
3 eqidd ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\to {A}×{B}={A}×{B}$
4 3 ancri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\to \left({A}×{B}={A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)$
5 2 4 impbii ${⊢}\left({A}×{B}={A}×{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}$
6 1 5 syl6bb ${⊢}\left({F}Fn\left({A}×{B}\right)\wedge {G}Fn\left({A}×{B}\right)\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}{x}{F}{y}={x}{G}{y}\right)$