In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import f, x, fx, A
from proveit.logic import Forall, Equals, SetOfAll, Image
```

In [2]:

```
%begin axioms
```

The image of a set under a function is the set obtained by applying the function to each element of that original set.

In [3]:

```
set_image_def = Forall(
(f, A), Equals(Image(f, A),
SetOfAll(x, fx, domain=A)))
```

In [4]:

```
%end axioms
```