Theorem rneq

Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996)

	Ref	Expression
Assertion	rneq	|- ( A = B -> ran A = ran B )

Proof

Step	Hyp	Ref	Expression
1		cnveq	|- ( A = B -> `' A = `' B )
2	1	dmeqd	|- ( A = B -> dom `' A = dom `' B )
3		df-rn	|- ran A = dom `' A
4		df-rn	|- ran B = dom `' B
5	2 3 4	3eqtr4g	|- ( A = B -> ran A = ran B )