Set identity (source code)

= Set identity

An equality between <sets> expressed in terms of arbitrary input <sets> that holds for every allowed choice of those inputs. A <double inclusion proof> proves a <set identity> by proving both <set inclusions>. Membership equivalences give another proof: the expressions are equal if and only if each element belongs to either both or neither.