This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oveq1

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

		Ref	Expression
	Assertion	oveq1	$⊢ A = B \to A F C = B F C$

Step	Hyp	Ref	Expression
1		opeq1	$⊢ A = B \to ⟨A, C⟩ = ⟨B, C⟩$
2	1	fveq2d	$⊢ A = B \to F (⟨A, C⟩) = F (⟨B, C⟩)$
3		df-ov	$⊢ A F C = F (⟨A, C⟩)$
4		df-ov	$⊢ B F C = F (⟨B, C⟩)$
5	2 3 4	3eqtr4g	$⊢ A = B \to A F C = B F C$