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

Metamath Proof Explorer

Theorem imaeq1

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994)

		Ref	Expression
	Assertion	imaeq1	$⊢ A = B \to A [C] = B [C]$

Step	Hyp	Ref	Expression
1		reseq1	$⊢ A = B \to {A ↾}_{C} = {B ↾}_{C}$
2	1	rneqd	$⊢ A = B \to ran ({A ↾}_{C}) = ran ({B ↾}_{C})$
3		df-ima	$⊢ A [C] = ran ({A ↾}_{C})$
4		df-ima	$⊢ B [C] = ran ({B ↾}_{C})$
5	2 3 4	3eqtr4g	$⊢ A = B \to A [C] = B [C]$