Theorem dmcnvcnv

Description: The domain of the double converse of a class is equal to its domain (even when that class in not a relation, in which case dfrel2 gives another proof). (Contributed by NM, 8-Apr-2007)

	Ref	Expression
Assertion	dmcnvcnv	|- dom `' `' A = dom A

Proof

Step	Hyp	Ref	Expression
1		dfdm4	|- dom A = ran `' A
2		df-rn	|- ran `' A = dom `' `' A
3	1 2	eqtr2i	|- dom `' `' A = dom A