Metamath Proof Explorer

Theorem resdm2

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

Ref Expression
Assertion resdm2 
|- ( A |` dom A ) = `' `' A

Proof

Step Hyp Ref Expression
1 rescnvcnv 
 |-  ( `' `' A |` dom `' `' A ) = ( A |` dom `' `' A )
2 relcnv 
 |-  Rel `' `' A
3 resdm 
 |-  ( Rel `' `' A -> ( `' `' A |` dom `' `' A ) = `' `' A )
4 2 3 ax-mp 
 |-  ( `' `' A |` dom `' `' A ) = `' `' A
5 dmcnvcnv 
 |-  dom `' `' A = dom A
6 5 reseq2i 
 |-  ( A |` dom `' `' A ) = ( A |` dom A )
7 1 4 6 3eqtr3ri 
 |-  ( A |` dom A ) = `' `' A