Metamath Proof Explorer


Theorem rncnvcnv

Description: The range of the double converse of a class is equal to its range (even when that class in not a relation). (Contributed by NM, 8-Apr-2007)

Ref Expression
Assertion rncnvcnv ranA-1-1=ranA

Proof

Step Hyp Ref Expression
1 df-rn ranA=domA-1
2 dfdm4 domA-1=ranA-1-1
3 1 2 eqtr2i ranA-1-1=ranA