Metamath Proof Explorer


Theorem afv2co2

Description: Value of a function composition, analogous to fvco2 . (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion afv2co2 G defAt X F defAt G '''' X F G '''' X = F '''' G '''' X

Proof

Step Hyp Ref Expression
1 imaco F G X = F G X
2 dfatsnafv2 G defAt X G '''' X = G X
3 2 adantr G defAt X F defAt G '''' X G '''' X = G X
4 3 imaeq2d G defAt X F defAt G '''' X F G '''' X = F G X
5 1 4 eqtr4id G defAt X F defAt G '''' X F G X = F G '''' X
6 5 eleq2d G defAt X F defAt G '''' X x F G X x F G '''' X
7 6 iotabidv G defAt X F defAt G '''' X ι x | x F G X = ι x | x F G '''' X
8 dfatco G defAt X F defAt G '''' X F G defAt X
9 dfafv23 F G defAt X F G '''' X = ι x | x F G X
10 8 9 syl G defAt X F defAt G '''' X F G '''' X = ι x | x F G X
11 dfafv23 F defAt G '''' X F '''' G '''' X = ι x | x F G '''' X
12 11 adantl G defAt X F defAt G '''' X F '''' G '''' X = ι x | x F G '''' X
13 7 10 12 3eqtr4d G defAt X F defAt G '''' X F G '''' X = F '''' G '''' X