Theorem rneqi

Description: Equality inference for range. (Contributed by NM, 4-Mar-2004)

	Ref	Expression
Hypothesis	rneqi.1	|- A = B
Assertion	rneqi	|- ran A = ran B

Proof

Step	Hyp	Ref	Expression
1		rneqi.1	|- A = B
2		rneq	|- ( A = B -> ran A = ran B )
3	1 2	ax-mp	|- ran A = ran B