Theorem ofeqd

Description: Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024)

	Ref	Expression
Hypothesis	ofeqd.1	⊢ ( 𝜑 → 𝑅 = 𝑆 )
Assertion	ofeqd	⊢ ( 𝜑 → ∘f 𝑅 = ∘f 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		ofeqd.1	⊢ ( 𝜑 → 𝑅 = 𝑆 )
2	1	oveqd	⊢ ( 𝜑 → ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) )
3	2	mpteq2dv	⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑆 ( 𝑔 ‘ 𝑥 ) ) ) )
4	3	mpoeq3dv	⊢ ( 𝜑 → ( 𝑓 ∈ 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 𝑆 )