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

Metamath Proof Explorer

Theorem fvoveq1

Description: Equality theorem for nested function and operation value. Closed form of fvoveq1d . (Contributed by AV, 23-Jul-2022)

		Ref	Expression
	Assertion	fvoveq1	$⊢ A = B \to F (A O C) = F (B O C)$

Step	Hyp	Ref	Expression
1		id	$⊢ A = B \to A = B$
2	1	fvoveq1d	$⊢ A = B \to F (A O C) = F (B O C)$