Description: Reverse closure law for function with the empty set not in its domain (if R = S ). (Contributed by NM, 26-Apr-1996) The class containing the function value does not have to be the domain. (Revised by Zhi Wang, 10-Nov-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ndmfvrcl.1 | |- dom F = S |
|
| ndmfvrcl.2 | |- -. (/) e. R |
||
| Assertion | ndmfvrcl | |- ( ( F ` A ) e. R -> A e. S ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ndmfvrcl.1 | |- dom F = S |
|
| 2 | ndmfvrcl.2 | |- -. (/) e. R |
|
| 3 | ndmfv | |- ( -. A e. dom F -> ( F ` A ) = (/) ) |
|
| 4 | 3 | eleq1d | |- ( -. A e. dom F -> ( ( F ` A ) e. R <-> (/) e. R ) ) |
| 5 | 2 4 | mtbiri | |- ( -. A e. dom F -> -. ( F ` A ) e. R ) |
| 6 | 5 | con4i | |- ( ( F ` A ) e. R -> A e. dom F ) |
| 7 | 6 1 | eleqtrdi | |- ( ( F ` A ) e. R -> A e. S ) |