ofeqd

Description: Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024)

		Ref	Expression
	Hypothesis	ofeqd.1	$⊢ φ \to R = S$
	Assertion	ofeqd	$⊢ φ \to \circ_{f} R = \circ_{f} S$

Step	Hyp	Ref	Expression
1		ofeqd.1	$⊢ φ \to R = S$
2	1	oveqd	$⊢ φ \to f (x) R g (x) = f (x) S g (x)$
3	2	mpteq2dv	$⊢ φ \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	mpoeq3dv	$⊢ φ \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	$⊢ φ \to \circ_{f} R = \circ_{f} S$

Metamath Proof Explorer