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 ⊢ φ → R = S
Assertion ofeqd ⊢ φ → ∘ f ⁡ R = ∘ f ⁡ S

Proof

Step Hyp Ref Expression
1 ofeqd.1 ⊢ φ → R = S
2 1 oveqd ⊢ φ → f ⁡ x R g ⁡ x = f ⁡ x S g ⁡ x
3 2 mpteq2dv ⊢ φ → x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x = x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x S g ⁡ x
4 3 mpoeq3dv ⊢ φ → f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x S g ⁡ x
5 df-of ⊢ ∘ f ⁡ R = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x R g ⁡ x
6 df-of ⊢ ∘ f ⁡ S = f ∈ V , g ∈ V ⟼ x ∈ dom ⁡ f ∩ dom ⁡ g ⟼ f ⁡ x S g ⁡ x
7 4 5 6 3eqtr4g ⊢ φ → ∘ f ⁡ R = ∘ f ⁡ S