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