Description: A function with removed elements is still a function. (Contributed by AV, 7-Jun-2021) Shorten proof and remove dependency on ax-sep and ax-pr . (Revised by Eric Schmidt, 24-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fundif | |- ( Fun F -> Fun ( F \ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | difss | |- ( F \ A ) C_ F |
|
| 2 | funss | |- ( ( F \ A ) C_ F -> ( Fun F -> Fun ( F \ A ) ) ) |
|
| 3 | 1 2 | ax-mp | |- ( Fun F -> Fun ( F \ A ) ) |