This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resindm

Description: When restricting a relation, intersecting with the domain of the relation has no effect. (Contributed by FL, 6-Oct-2008)

Ref Expression
Assertion resindm 
|- ( Rel A -> ( A |` ( B i^i dom A ) ) = ( A |` B ) )

Proof

Step Hyp Ref Expression
1 resdm 
 |-  ( Rel A -> ( A |` dom A ) = A )
2 1 ineq2d 
 |-  ( Rel A -> ( ( A |` B ) i^i ( A |` dom A ) ) = ( ( A |` B ) i^i A ) )
3 resindi 
 |-  ( A |` ( B i^i dom A ) ) = ( ( A |` B ) i^i ( A |` dom A ) )
4 incom 
 |-  ( ( A |` B ) i^i A ) = ( A i^i ( A |` B ) )
5 inres 
 |-  ( A i^i ( A |` B ) ) = ( ( A i^i A ) |` B )
6 inidm 
 |-  ( A i^i A ) = A
7 6 reseq1i 
 |-  ( ( A i^i A ) |` B ) = ( A |` B )
8 4 5 7 3eqtrri 
 |-  ( A |` B ) = ( ( A |` B ) i^i A )
9 2 3 8 3eqtr4g 
 |-  ( Rel A -> ( A |` ( B i^i dom A ) ) = ( A |` B ) )