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