Metamath Proof Explorer

Theorem ofceq

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

Ref Expression
Assertion ofceq ⊢ R = S → ∘ fc ⁡ R = ∘ fc ⁡ S

Proof

Step Hyp Ref Expression
1 oveq ⊢ R = S → f ⁡ x R c = f ⁡ x S c
2 1 mpteq2dv ⊢ R = S → x ∈ dom ⁡ f ⟼ f ⁡ x R c = x ∈ dom ⁡ f ⟼ f ⁡ x S c
3 2 mpoeq3dv ⊢ R = S → f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x S c
4 df-ofc ⊢ ∘ fc ⁡ R = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x R c
5 df-ofc ⊢ ∘ fc ⁡ S = f ∈ V , c ∈ V ⟼ x ∈ dom ⁡ f ⟼ f ⁡ x S c
6 3 4 5 3eqtr4g ⊢ R = S → ∘ fc ⁡ R = ∘ fc ⁡ S