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 G Fn A X A F G X = F G X

Proof

Step Hyp Ref Expression
1 imaco F G X = F G X
2 fnsnfv G Fn A X A G X = G X
3 2 imaeq2d G Fn A X A F G X = F G X
4 1 3 eqtr4id G Fn A X A F G X = F G X
5 4 eleq2d G Fn A X A x F G X x F G X
6 5 iotabidv G Fn A X A ι x | x F G X = ι x | x F G X
7 dffv3 F G X = ι x | x F G X
8 dffv3 F G X = ι x | x F G X
9 6 7 8 3eqtr4g G Fn A X A F G X = F G X