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 𝐴 → ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		resdm	⊢ ( Rel 𝐴 → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )
2	1	ineq2d	⊢ ( Rel 𝐴 → ( ( 𝐴 ↾ 𝐵 ) ∩ ( 𝐴 ↾ dom 𝐴 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∩ 𝐴 ) )
3		resindi	⊢ ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( ( 𝐴 ↾ 𝐵 ) ∩ ( 𝐴 ↾ dom 𝐴 ) )
4		incom	⊢ ( ( 𝐴 ↾ 𝐵 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝐴 ↾ 𝐵 ) )
5		inres	⊢ ( 𝐴 ∩ ( 𝐴 ↾ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐴 ) ↾ 𝐵 )
6		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
7	6	reseq1i	⊢ ( ( 𝐴 ∩ 𝐴 ) ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 )
8	4 5 7	3eqtrri	⊢ ( 𝐴 ↾ 𝐵 ) = ( ( 𝐴 ↾ 𝐵 ) ∩ 𝐴 )
9	2 3 8	3eqtr4g	⊢ ( Rel 𝐴 → ( 𝐴 ↾ ( 𝐵 ∩ dom 𝐴 ) ) = ( 𝐴 ↾ 𝐵 ) )