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

Metamath Proof Explorer

Theorem cnvimarndm

Description: The preimage of the range of a class is the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009)

Ref Expression
Assertion cnvimarndm ⊢ A -1 ran ⁡ A = dom ⁡ A

Proof

Step Hyp Ref Expression
1 imadmrn ⊢ A -1 dom ⁡ A -1 = ran ⁡ A -1
2 df-rn ⊢ ran ⁡ A = dom ⁡ A -1
3 2 imaeq2i ⊢ A -1 ran ⁡ A = A -1 dom ⁡ A -1
4 dfdm4 ⊢ dom ⁡ A = ran ⁡ A -1
5 1 3 4 3eqtr4i ⊢ A -1 ran ⁡ A = dom ⁡ A