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	|- ( A e. dom F -> dom ( F |` { A } ) = { A } )

Proof

Step	Hyp	Ref	Expression
1		dmres	|- dom ( F |` { A } ) = ( { A } i^i dom F )
2		snssi	|- ( A e. dom F -> { A } C_ dom F )
3		df-ss	|- ( { A } C_ dom F <-> ( { A } i^i dom F ) = { A } )
4	2 3	sylib	|- ( A e. dom F -> ( { A } i^i dom F ) = { A } )
5	1 4	syl5eq	|- ( A e. dom F -> dom ( F |` { A } ) = { A } )