# Metamath Proof Explorer

## Theorem fvco2

Description: Value of a function composition. Similar to second part of Theorem 3H of Enderton p. 47. (Contributed by NM, 9-Oct-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by Stefan O'Rear, 16-Oct-2014)

Ref Expression
Assertion fvco2 ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left({F}\circ {G}\right)\left({X}\right)={F}\left({G}\left({X}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fnsnfv ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left\{{G}\left({X}\right)\right\}={G}\left[\left\{{X}\right\}\right]$
2 1 imaeq2d ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to {F}\left[\left\{{G}\left({X}\right)\right\}\right]={F}\left[{G}\left[\left\{{X}\right\}\right]\right]$
3 imaco ${⊢}\left({F}\circ {G}\right)\left[\left\{{X}\right\}\right]={F}\left[{G}\left[\left\{{X}\right\}\right]\right]$
4 2 3 syl6reqr ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left({F}\circ {G}\right)\left[\left\{{X}\right\}\right]={F}\left[\left\{{G}\left({X}\right)\right\}\right]$
5 4 eleq2d ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left({x}\in \left({F}\circ {G}\right)\left[\left\{{X}\right\}\right]↔{x}\in {F}\left[\left\{{G}\left({X}\right)\right\}\right]\right)$
6 5 iotabidv ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left(\iota {x}|{x}\in \left({F}\circ {G}\right)\left[\left\{{X}\right\}\right]\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{G}\left({X}\right)\right\}\right]\right)$
7 dffv3 ${⊢}\left({F}\circ {G}\right)\left({X}\right)=\left(\iota {x}|{x}\in \left({F}\circ {G}\right)\left[\left\{{X}\right\}\right]\right)$
8 dffv3 ${⊢}{F}\left({G}\left({X}\right)\right)=\left(\iota {x}|{x}\in {F}\left[\left\{{G}\left({X}\right)\right\}\right]\right)$
9 6 7 8 3eqtr4g ${⊢}\left({G}Fn{A}\wedge {X}\in {A}\right)\to \left({F}\circ {G}\right)\left({X}\right)={F}\left({G}\left({X}\right)\right)$