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.logic import Forall, And, Equals, InSet, SetOfAll, Exists
from proveit import n, x, Q, f, Qy
from proveit.core_expr_types import y_1_to_n, f__y_1_to_n, Q__y_1_to_n, S_1_to_n
from proveit.logic.sets import general_comprehension_fyn
from proveit.numbers import Exp, Natural, NaturalPos
%begin axioms
```

**Define general set comprehension any mapping $y \mapsto f(y)$ applied to the set of elements $y$ of $S$ such that $Q(y)$:**
TODO: CHANGE THIS TO A DEFINITION USING UnionOfAll:
{f(x) | Q(x)}*{x in S} = Union*{x in S | Q(x)} {f(x)}

In [2]:

```
comprehension_def = Forall(n,
Forall((S_1_to_n, Q, f, x),
Equals(InSet(x, general_comprehension_fyn),
Exists(y_1_to_n, Equals(x, f__y_1_to_n),
domains=[S_1_to_n], conditions=[Q__y_1_to_n]))\
.with_wrap_before_operator()),
domain=NaturalPos)
```

NOTE: Comprehension defines a subset of some set $S$, and a "universal" set must not be allowed. Otherwise you could define Russell's set, $R = \{x~|~x \notin x\}_x$, which results in paradox upon asking whether or not $R \in R$ (if it is, then it cannot be; if it is not, then it must be). But if $x \in S$ can only be true if $S$ is a "properly" defined set which cannot contain itself, then Russell's paradox is avoided. Note that, although using the same notation in formatting, set membership is distinct from class membership, and we *cannot* apply subset comprehension to proper classes.

In [3]:

```
%end axioms
```