# Metamath Proof Explorer

## Theorem eqfnfvd

Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses eqfnfvd.1 ${⊢}{\phi }\to {F}Fn{A}$
eqfnfvd.2 ${⊢}{\phi }\to {G}Fn{A}$
eqfnfvd.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={G}\left({x}\right)$
Assertion eqfnfvd ${⊢}{\phi }\to {F}={G}$

### Proof

Step Hyp Ref Expression
1 eqfnfvd.1 ${⊢}{\phi }\to {F}Fn{A}$
2 eqfnfvd.2 ${⊢}{\phi }\to {G}Fn{A}$
3 eqfnfvd.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={G}\left({x}\right)$
4 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)$
5 eqfnfv ${⊢}\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)$
6 1 2 5 syl2anc ${⊢}{\phi }\to \left({F}={G}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)={G}\left({x}\right)\right)$
7 4 6 mpbird ${⊢}{\phi }\to {F}={G}$