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 GFnAXAFGX=FGX

Proof

Step Hyp Ref Expression
1 imaco FGX=FGX
2 fnsnfv GFnAXAGX=GX
3 2 imaeq2d GFnAXAFGX=FGX
4 1 3 eqtr4id GFnAXAFGX=FGX
5 4 eleq2d GFnAXAxFGXxFGX
6 5 iotabidv GFnAXAιx|xFGX=ιx|xFGX
7 dffv3 FGX=ιx|xFGX
8 dffv3 FGX=ιx|xFGX
9 6 7 8 3eqtr4g GFnAXAFGX=FGX