# Metamath Proof Explorer

## Theorem fnhomeqhomf

Description: If the Hom-set operation is a function it is equal to the corresponding functionalized Hom-set operation. (Contributed by AV, 1-Mar-2020)

Ref Expression
Hypotheses homffval.f ${⊢}{F}={\mathrm{Hom}}_{𝑓}\left({C}\right)$
homffval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
homffval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
Assertion fnhomeqhomf ${⊢}{H}Fn\left({B}×{B}\right)\to {F}={H}$

### Proof

Step Hyp Ref Expression
1 homffval.f ${⊢}{F}={\mathrm{Hom}}_{𝑓}\left({C}\right)$
2 homffval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
3 homffval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
4 fnov ${⊢}{H}Fn\left({B}×{B}\right)↔{H}=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)$
5 1 2 3 homffval ${⊢}{F}=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)$
6 eqeq2 ${⊢}{H}=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)\to \left({F}={H}↔{F}=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)\right)$
7 5 6 mpbiri ${⊢}{H}=\left({x}\in {B},{y}\in {B}⟼{x}{H}{y}\right)\to {F}={H}$
8 4 7 sylbi ${⊢}{H}Fn\left({B}×{B}\right)\to {F}={H}$