This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = dom A

Proof

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