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

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

%begin axioms

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

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

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

set_equiv_def:

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

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

set_not_equiv_def:

%end axioms

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