| 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 6736 | . 2 ⊢ (𝐺:𝐴⟶𝐵 → 𝐺 Fn 𝐴) | |
| 2 | fvco2 7006 | . 2 ⊢ ((𝐺 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ ((𝐺:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝐶) = (𝐹‘(𝐺‘𝐶))) |
| Copyright terms: Public domain | W3C validator |