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 φ A V
offveq.2 φ F Fn A
offveq.3 φ G Fn A
offveq.4 φ H Fn A
offveq.5 φ x A F x = B
offveq.6 φ x A G x = C
offveq.7 φ x A B R C = H x
Assertion offveq φ F R f G = H

Proof

Step Hyp Ref Expression
1 offveq.1 φ A V
2 offveq.2 φ F Fn A
3 offveq.3 φ G Fn A
4 offveq.4 φ H Fn A
5 offveq.5 φ x A F x = B
6 offveq.6 φ x A G x = C
7 offveq.7 φ x A B R C = H x
8 inidm A A = A
9 2 3 1 1 8 offn φ F R f G Fn A
10 2 3 1 1 8 5 6 ofval φ x A F R f G x = B R C
11 10 7 eqtrd φ x A F R f G x = H x
12 9 4 11 eqfnfvd φ F R f G = H