Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Functions
fvcod
Next ⟩
freld
Metamath Proof Explorer
Ascii
Unicode
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