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

Metamath Proof Explorer

Theorem resdm

Description: A relation restricted to its domain equals itself. (Contributed by NM, 12-Dec-2006)

Ref Expression
Assertion resdm ⊢ Rel ⁡ A → A ↾ dom ⁡ A = A

Proof

Step Hyp Ref Expression
1 ssid ⊢ dom ⁡ A ⊆ dom ⁡ A
2 relssres ⊢ Rel ⁡ A ∧ dom ⁡ A ⊆ dom ⁡ A → A ↾ dom ⁡ A = A
3 1 2 mpan2 ⊢ Rel ⁡ A → A ↾ dom ⁡ A = A