Theorem cnvimarndmOLD

Description: Obsolete version of cnvimarndm as of 29-Sep-2026. (Contributed by Jeff Hankins, 15-Jul-2009) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cnvimarndmOLD	|- ( `' A " ran A ) = dom A

Proof

Step	Hyp	Ref	Expression
1		imadmrn	|- ( `' A " dom `' A ) = ran `' A
2		df-rn	|- ran A = dom `' A
3	2	imaeq2i	|- ( `' A " ran A ) = ( `' A " dom `' A )
4		dfdm4	|- dom A = ran `' A
5	1 3 4	3eqtr4i	|- ( `' A " ran A ) = dom A