# Metamath Proof Explorer

## Theorem fnfvof

Description: Function value of a pointwise composition. (Contributed by Stefan O'Rear, 5-Oct-2014) (Proof shortened by Mario Carneiro, 5-Jun-2015)

Ref Expression
Assertion fnfvof ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge \left({A}\in {V}\wedge {X}\in {A}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\left({X}\right)={F}\left({X}\right){R}{G}\left({X}\right)$

### Proof

Step Hyp Ref Expression
1 simpll ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\to {F}Fn{A}$
2 simplr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\to {G}Fn{A}$
3 simpr ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\to {A}\in {V}$
4 inidm ${⊢}{A}\cap {A}={A}$
5 eqidd ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\wedge {X}\in {A}\right)\to {F}\left({X}\right)={F}\left({X}\right)$
6 eqidd ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\wedge {X}\in {A}\right)\to {G}\left({X}\right)={G}\left({X}\right)$
7 1 2 3 3 4 5 6 ofval ${⊢}\left(\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge {A}\in {V}\right)\wedge {X}\in {A}\right)\to \left({F}{{R}}_{f}{G}\right)\left({X}\right)={F}\left({X}\right){R}{G}\left({X}\right)$
8 7 anasss ${⊢}\left(\left({F}Fn{A}\wedge {G}Fn{A}\right)\wedge \left({A}\in {V}\wedge {X}\in {A}\right)\right)\to \left({F}{{R}}_{f}{G}\right)\left({X}\right)={F}\left({X}\right){R}{G}\left({X}\right)$