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 ∩ dom ⁡ A = A ↾ B

Proof

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