Theorem resdm2

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

	Ref	Expression
Assertion	resdm2	⊢ ( 𝐴 ↾ dom 𝐴 ) = ◡ ◡ 𝐴

Proof

Step	Hyp	Ref	Expression
1		rescnvcnv	⊢ ( ◡ ◡ 𝐴 ↾ dom ◡ ◡ 𝐴 ) = ( 𝐴 ↾ dom ◡ ◡ 𝐴 )
2		relcnv	⊢ Rel ◡ ◡ 𝐴
3		resdm	⊢ ( Rel ◡ ◡ 𝐴 → ( ◡ ◡ 𝐴 ↾ dom ◡ ◡ 𝐴 ) = ◡ ◡ 𝐴 )
4	2 3	ax-mp	⊢ ( ◡ ◡ 𝐴 ↾ dom ◡ ◡ 𝐴 ) = ◡ ◡ 𝐴
5		dmcnvcnv	⊢ dom ◡ ◡ 𝐴 = dom 𝐴
6	5	reseq2i	⊢ ( 𝐴 ↾ dom ◡ ◡ 𝐴 ) = ( 𝐴 ↾ dom 𝐴 )
7	1 4 6	3eqtr3ri	⊢ ( 𝐴 ↾ dom 𝐴 ) = ◡ ◡ 𝐴