Metamath Proof Explorer


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