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 x, A, B, X
from proveit.logic import And, Equals, Forall, in_bool, Not, InSet
from proveit.logic.sets import SubsetEq, SetEquiv, SetNotEquiv
```

In [2]:

```
%begin axioms
```

**By definition, two sets are equivalent if they contain the same elements.

In [3]:

```
set_equiv_def = Forall((A, B), Equals(SetEquiv(A, B), Forall(x, Equals(InSet(x, A), InSet(x, B)))))
```

**Define $A \ncong B$ as $\lnot (A \cong B)$:**

In [4]:

```
set_not_equiv_def = Forall((A, B), Equals(SetNotEquiv(A, B), Not(SetEquiv(A, B))))
```

In [5]:

```
%end axioms
```