Metamath Proof Explorer

Theorem eqfnfv2f

Description: Equality of functions is determined by their values. Special case of Exercise 4 of TakeutiZaring p. 28 (with domain equality omitted). This version of eqfnfv uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 29-Jan-2004)

Ref Expression
Hypotheses eqfnfv2f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
eqfnfv2f.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{G}$
Assertion eqfnfv2f ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$

Proof

Step Hyp Ref Expression
1 eqfnfv2f.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}$
2 eqfnfv2f.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{G}$
3 eqfnfv ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left({F}={G}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={G}\left({z}\right)\right)$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
5 1 4 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)$
6 2 4 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{G}\left({z}\right)$
7 5 6 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={G}\left({z}\right)$
8 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)$
9 fveq2 ${⊢}{z}={x}\to {F}\left({z}\right)={F}\left({x}\right)$
10 fveq2 ${⊢}{z}={x}\to {G}\left({z}\right)={G}\left({x}\right)$
11 9 10 eqeq12d ${⊢}{z}={x}\to \left({F}\left({z}\right)={G}\left({z}\right)↔{F}\left({x}\right)={G}\left({x}\right)\right)$
12 7 8 11 cbvralw ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)={G}\left({z}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)$
13 3 12 syl6bb ${⊢}\left({F}Fn{A}\wedge {G}Fn{A}\right)\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$