Existential quantification is a general expression about *something* (`Exists`

: $\exists$).

The `Exists`

**Expression** derives from `OperationOverInstances`

. As such, it has instance variables (`instance_vars`

) with an instance expression (`instance_expr`

) and may be restricted to a `domain`

and have zero or more `conditions`

. For example $\exists_{x, y \in S~|~Q(x, y),~R(y)} P(x, y)$ means that $P(x, y)$ is `TRUE`

for some occurrence of $x$ and $y$ in domain $S$ for which the conditions $Q(x, y)$ and $R(y)$ are satisfied. The `conditions`

may be any **Expression**s involving the instance variables.

The negation of the existential quantification is compactly expressed as $\nexists$, represented by the `NotExists`

**Expression** type.

In [1]:

```
import proveit
%theory
```