Theorem resdm2

Description: A class restricted to its domain equals its double converse. (Contributed by NM, 8-Apr-2007)

	Ref	Expression
Assertion	resdm2	$$⊢{A\upharpoonright }_{\mathrm{dom}A}={A^{-1}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		rescnvcnv	$$⊢{{A^{-1}}^{-1}\upharpoonright }_{\mathrm{dom}{A^{-1}}^{-1}}={A\upharpoonright }_{\mathrm{dom}{A^{-1}}^{-1}}$$
2		relcnv	$$⊢\mathrm{Rel}{A^{-1}}^{-1}$$
3		resdm	$$⊢\mathrm{Rel}{A^{-1}}^{-1}\to {{A^{-1}}^{-1}\upharpoonright }_{\mathrm{dom}{A^{-1}}^{-1}}={A^{-1}}^{-1}$$
4	2 3	ax-mp	$$⊢{{A^{-1}}^{-1}\upharpoonright }_{\mathrm{dom}{A^{-1}}^{-1}}={A^{-1}}^{-1}$$
5		dmcnvcnv	$$⊢\mathrm{dom}{A^{-1}}^{-1}=\mathrm{dom}A$$
6	5	reseq2i	$$⊢{A\upharpoonright }_{\mathrm{dom}{A^{-1}}^{-1}}={A\upharpoonright }_{\mathrm{dom}A}$$
7	1 4 6	3eqtr3ri	$$⊢{A\upharpoonright }_{\mathrm{dom}A}={A^{-1}}^{-1}$$