Metamath Proof Explorer


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 )