Theorem ofeq

Description: Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)

	Ref	Expression
Assertion	ofeq	⊢ ( 𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑅 = 𝑆 ∧ 𝑓 ∈ V ∧ 𝑔 ∈ V ) → 𝑅 = 𝑆 )
2	1	oveqd	⊢ ( ( 𝑅 = 𝑆 ∧ 𝑓 ∈ V ∧ 𝑔 ∈ V ) → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) )
3	2	mpteq2dv	⊢ ( ( 𝑅 = 𝑆 ∧ 𝑓 ∈ V ∧ 𝑔 ∈ V ) → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) ) )
4	3	mpoeq3dva	⊢ ( 𝑅 = 𝑆 → ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) ) = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) ) ) )
5		df-of	⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
6		df-of	⊢ ∘f 𝑆 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) ) )
7	4 5 6	3eqtr4g	⊢ ( 𝑅 = 𝑆 → ∘f 𝑅 = ∘f 𝑆 )