This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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		id	$⊢ R = S \to R = S$
2	1	ofeqd	$⊢ R = S \to \circ_{f} R = \circ_{f} S$