# Metamath Proof Explorer

## Theorem offveq

Description: Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses offveq.1 ${⊢}{\phi }\to {A}\in {V}$
offveq.2 ${⊢}{\phi }\to {F}Fn{A}$
offveq.3 ${⊢}{\phi }\to {G}Fn{A}$
offveq.4 ${⊢}{\phi }\to {H}Fn{A}$
offveq.5 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={B}$
offveq.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {G}\left({x}\right)={C}$
offveq.7 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}{R}{C}={H}\left({x}\right)$
Assertion offveq ${⊢}{\phi }\to {F}{{R}}_{f}{G}={H}$

### Proof

Step Hyp Ref Expression
1 offveq.1 ${⊢}{\phi }\to {A}\in {V}$
2 offveq.2 ${⊢}{\phi }\to {F}Fn{A}$
3 offveq.3 ${⊢}{\phi }\to {G}Fn{A}$
4 offveq.4 ${⊢}{\phi }\to {H}Fn{A}$
5 offveq.5 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)={B}$
6 offveq.6 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {G}\left({x}\right)={C}$
7 offveq.7 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}{R}{C}={H}\left({x}\right)$
8 inidm ${⊢}{A}\cap {A}={A}$
9 2 3 1 1 8 offn ${⊢}{\phi }\to \left({F}{{R}}_{f}{G}\right)Fn{A}$
10 2 3 1 1 8 5 6 ofval ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({F}{{R}}_{f}{G}\right)\left({x}\right)={B}{R}{C}$
11 10 7 eqtrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({F}{{R}}_{f}{G}\right)\left({x}\right)={H}\left({x}\right)$
12 9 4 11 eqfnfvd ${⊢}{\phi }\to {F}{{R}}_{f}{G}={H}$