**Description:** Equality theorem for operation value. (Contributed by NM, 28-Feb-1995)

Ref | Expression | ||
---|---|---|---|

Assertion | oveq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 𝐹 𝐴 ) = ( 𝐶 𝐹 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | opeq2 | ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐶 , 𝐴 ⟩ = ⟨ 𝐶 , 𝐵 ⟩ ) | |

2 | 1 | fveq2d | ⊢ ( 𝐴 = 𝐵 → ( 𝐹 ‘ ⟨ 𝐶 , 𝐴 ⟩ ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝐵 ⟩ ) ) |

3 | df-ov | ⊢ ( 𝐶 𝐹 𝐴 ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝐴 ⟩ ) | |

4 | df-ov | ⊢ ( 𝐶 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐶 , 𝐵 ⟩ ) | |

5 | 2 3 4 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 𝐹 𝐴 ) = ( 𝐶 𝐹 𝐵 ) ) |