Description: Equality theorem for range. (Contributed by NM, 29Dec1996)
Ref  Expression  

Assertion  rneq   ( A = B > ran A = ran B ) 
Step  Hyp  Ref  Expression 

1  cnveq   ( A = B > `' A = `' B ) 

2  1  dmeqd   ( A = B > dom `' A = dom `' B ) 
3  dfrn   ran A = dom `' A 

4  dfrn   ran B = dom `' B 

5  2 3 4  3eqtr4g   ( A = B > ran A = ran B ) 