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	$$⊢\mathrm{dom}{A^{-1}}^{-1}=\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
2		df-rn	$$⊢\mathrm{ran}{A}^{-1}=\mathrm{dom}{A^{-1}}^{-1}$$
3	1 2	eqtr2i	$$⊢\mathrm{dom}{A^{-1}}^{-1}=\mathrm{dom}A$$