集合外延性公理

一个集合由“哪些对象是它的成员”决定，没有成员列表之外的隐藏身份。排列、重复列写、描述方法和构造历史不参与集合相等。例如 $\{1,2,2\}=\{2,1\}$，因为任取一个对象，它属于左边恰好也属于右边。

这个原则只适用于正在讨论的集合对象。序列 $(1,2)$ 与 $(2,1)$ 不相等，因为位置属于序列结构；多重集合还记录出现次数。不能把集合对顺序和次数的忽略，不加说明地推广到这些不同对象。

用双向包含证明不交分解 ​

把 $A$ 的成员按是否属于 $B$ 分开，可以得到

先证左边包含于右边。任取 $x\in (A\setminus B)\cup (A\cap B)$。若 $x\in A\setminus B$，差集的定义给出 $x\in A$；若 $x\in A\cap B$，交集的定义也给出 $x\in A$。因此左边的每个元素都属于 $A$。

再证右边包含于左边。任取 $x\in A$，按成员判断的排中律分两种情况：若 $x\in B$，则 $x\in A\cap B$；若 $x\notin B$，则 $x\in A\setminus B$。无论哪种情况，$x$ 都属于这两部分的并。

两次论证中的 $x$ 都是任意选取的，所以得到双向包含，外延性据此给出集合相等。两部分还互不相交：若一个对象同时属于它们，就必须同时满足 $x\in B$ 与 $x\notin B$。因此这既是集合相等的证明，也是将 $A$ 分成两个不重复部分的证书；从 $A$ 到并集的方向显式使用了经典逻辑的排中律。

唯一性不等于存在性 ​

若 $E$、$F$ 都没有元素，则对所有 $x$，$x\in E$ 与 $x\in F$ 都为假，故 $E=F$。这证明空集至多一个，却没有单凭外延性制造出空集。空集、配对集、幂集以及运算结果的存在，仍需其他集合论公理。

同样，“满足某条件的所有对象”不能无条件组成集合。若假定存在 $R=\{x:x\notin x\}$，代入 $x=R$ 就得到 $R\in R\leftrightarrow R\notin R$。这是不受限制的概括原则出错，不是外延性失效。

子集理路子集Subset · Set inclusionA 的每个元素都属于 B 时成立的包含关系；它在集合之间形成偏序。给出双向包含的证明形式；逻辑等价理路逻辑等价Logical equivalence两个公式在指定语义类的每个结构与赋值下具有相同真值。则允许把集合运算恒等式变成成员命题的等价。前者适合两边结构差异较大时分别证明，后者适合直接展开并、交、补等运算。

关系可以编码为有序对的集合，因此关系相等也能逐对检查。对函数则必须遵守本库的约定：函数理路函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。还带有定义域和陪域，两个函数图相等之外，也须核对声明的定义域与陪域；集合外延性并不取消这些类型数据。