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	⊢ ( 𝐴 = 𝐵 → ( 𝐹 ‘ ( 𝐴 𝑂 𝐶 ) ) = ( 𝐹 ‘ ( 𝐵 𝑂 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
2	1	fvoveq1d	⊢ ( 𝐴 = 𝐵 → ( 𝐹 ‘ ( 𝐴 𝑂 𝐶 ) ) = ( 𝐹 ‘ ( 𝐵 𝑂 𝐶 ) ) )