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

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

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

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

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

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

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

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

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