![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvco3 | Structured version Visualization version GIF version |
Description: Value of a function composition. (Contributed by NM, 3-Jan-2004.) (Revised by Mario Carneiro, 26-Dec-2014.) |
Ref | Expression |
---|---|
fvco3 | ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 6669 | . 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴) | |
2 | fvco2 6939 | . 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | |
3 | 1, 2 | sylan 581 | 1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
Copyright terms: Public domain | W3C validator |