This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvcod

Description: Value of a function composition. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses fvcod.g ⊢ φ → Fun ⁡ G
fvcod.a ⊢ φ → A ∈ dom ⁡ G
fvcod.h ⊢ H = F ∘ G
Assertion fvcod ⊢ φ → H ⁡ A = F ⁡ G ⁡ A

Proof

Step Hyp Ref Expression
1 fvcod.g ⊢ φ → Fun ⁡ G
2 fvcod.a ⊢ φ → A ∈ dom ⁡ G
3 fvcod.h ⊢ H = F ∘ G
4 3 fveq1i ⊢ H ⁡ A = F ∘ G ⁡ A
5 4 a1i ⊢ φ → H ⁡ A = F ∘ G ⁡ A
6 fvco ⊢ Fun ⁡ G ∧ A ∈ dom ⁡ G → F ∘ G ⁡ A = F ⁡ G ⁡ A
7 1 2 6 syl2anc ⊢ φ → F ∘ G ⁡ A = F ⁡ G ⁡ A
8 5 7 eqtrd ⊢ φ → H ⁡ A = F ⁡ G ⁡ A