Metamath Proof Explorer

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