Theorem resdm

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

	Ref	Expression
Assertion	resdm	⊢ ( Rel 𝐴 → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ dom 𝐴 ⊆ dom 𝐴
2		relssres	⊢ ( ( Rel 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴 ) → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )
3	1 2	mpan2	⊢ ( Rel 𝐴 → ( 𝐴 ↾ dom 𝐴 ) = 𝐴 )