Description: Equality inference for range. (Contributed by NM, 4Mar2004)
Ref  Expression  

Hypothesis  rneqi.1   A = B 

Assertion  rneqi   ran A = ran B 
Step  Hyp  Ref  Expression 

1  rneqi.1   A = B 

2  rneq   ( A = B > ran A = ran B ) 

3  1 2  axmp   ran A = ran B 