ofeq

Description: Equality theorem for function operation. (Contributed by Mario Carneiro, 20-Jul-2014)

		Ref	Expression
	Assertion	ofeq	$⊢ R = S \to \circ_{f} R = \circ_{f} S$

Step	Hyp	Ref	Expression
1		simp1	$⊢ (R = S \land f \in V \land g \in V) \to R = S$
2	1	oveqd	$⊢ (R = S \land f \in V \land g \in V) \to f (x) R g (x) = f (x) S g (x)$
3	2	mpteq2dv	$⊢ (R = S \land f \in V \land g \in V) \to (x \in (dom f \cap dom g) ⟼ f (x) R g (x)) = (x \in (dom f \cap dom g) ⟼ f (x) S g (x))$
4	3	mpoeq3dva	$⊢ R = S \to (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x))) = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) S g (x)))$
5		df-of	$⊢ \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
6		df-of	$⊢ \circ_{f} S = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) S g (x)))$
7	4 5 6	3eqtr4g	$⊢ R = S \to \circ_{f} R = \circ_{f} S$

Metamath Proof Explorer