Theorem ofceq

Description: Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Assertion	ofceq	⊢ ( 𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		oveq	⊢ ( 𝑅 = 𝑆 → ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) = ( ( 𝑓 ‘ 𝑥 ) 𝑆 𝑐 ) )
2	1	mpteq2dv	⊢ ( 𝑅 = 𝑆 → ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) = ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 𝑐 ) ) )
3	2	mpoeq3dv	⊢ ( 𝑅 = 𝑆 → ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) ) = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 𝑐 ) ) ) )
4		df-ofc	⊢ ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )
5		df-ofc	⊢ ∘f/c 𝑆 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 𝑐 ) ) )
6	3 4 5	3eqtr4g	⊢ ( 𝑅 = 𝑆 → ∘f/c 𝑅 = ∘f/c 𝑆 )