Description: The value of a non-member of a restriction is the empty set. (An artifact of our function value definition.) (Contributed by NM, 13-Nov-1995)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfvres | |- ( -. A e. B -> ( ( F |` B ) ` A ) = (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dmres | |- dom ( F |` B ) = ( B i^i dom F ) |
|
| 2 | inss1 | |- ( B i^i dom F ) C_ B |
|
| 3 | 1 2 | eqsstri | |- dom ( F |` B ) C_ B |
| 4 | 3 | sseli | |- ( A e. dom ( F |` B ) -> A e. B ) |
| 5 | ndmfv | |- ( -. A e. dom ( F |` B ) -> ( ( F |` B ) ` A ) = (/) ) |
|
| 6 | 4 5 | nsyl5 | |- ( -. A e. B -> ( ( F |` B ) ` A ) = (/) ) |