Metamath Proof Explorer

Theorem imaeq2

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

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

Proof

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