ofceq

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

		Ref	Expression
	Assertion	ofceq	$⊢ R = S \to \circ_{fc} R = \circ_{fc} S$

Step	Hyp	Ref	Expression
1		oveq	$⊢ R = S \to f (x) R c = f (x) S c$
2	1	mpteq2dv	$⊢ R = S \to (x \in dom f ⟼ f (x) R c) = (x \in dom f ⟼ f (x) S c)$
3	2	mpoeq3dv	$⊢ R = S \to (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c)) = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) S c))$
4		df-ofc	$⊢ \circ_{fc} R = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) R c))$
5		df-ofc	$⊢ \circ_{fc} S = (f \in V, c \in V ⟼ (x \in dom f ⟼ f (x) S c))$
6	3 4 5	3eqtr4g	$⊢ R = S \to \circ_{fc} R = \circ_{fc} S$

Metamath Proof Explorer