Theorem dmressnsn

Description: The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017)

	Ref	Expression
Assertion	dmressnsn	⊢ ( 𝐴 ∈ dom 𝐹 → dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		dmres	⊢ dom ( 𝐹 ↾ { 𝐴 } ) = ( { 𝐴 } ∩ dom 𝐹 )
2		snssi	⊢ ( 𝐴 ∈ dom 𝐹 → { 𝐴 } ⊆ dom 𝐹 )
3		df-ss	⊢ ( { 𝐴 } ⊆ dom 𝐹 ↔ ( { 𝐴 } ∩ dom 𝐹 ) = { 𝐴 } )
4	2 3	sylib	⊢ ( 𝐴 ∈ dom 𝐹 → ( { 𝐴 } ∩ dom 𝐹 ) = { 𝐴 } )
5	1 4	eqtrid	⊢ ( 𝐴 ∈ dom 𝐹 → dom ( 𝐹 ↾ { 𝐴 } ) = { 𝐴 } )