Axioms for the theory of proveit.logic.sets.subtraction

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, Equals, And, InSet, NotInSet, Difference
from proveit import A, B, x
%begin axioms

Defining axioms for theory 'proveit.logic.sets.subtraction'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

The difference of two sets includes all of the members of the minuend (first operand) except those contained in the subtrahend (second operand):

difference_def = Forall((x, A, B), Equals(InSet(x, Difference(A, B)),
                                         And(InSet(x, A), NotInSet(x, B))))

difference_def:

%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.subtraction