Metamath Proof Explorer


Theorem rncnv

Description: Range of converse is the domain. (Contributed by Peter Mazsa, 12-Feb-2018)

Ref Expression
Assertion rncnv ran A -1 = dom A

Proof

Step Hyp Ref Expression
1 dfdm4 dom A = ran A -1
2 1 eqcomi ran A -1 = dom A