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

Metamath Proof Explorer

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 𝑆 )