嗨，我来帮你梳理这些公理在ZFC里的实际应用——其实它们不像表面看起来那样“没用”，而是藏在ZFC公理的表述和推导的底层逻辑里，咱们一个个拆解来看：

一、一阶逻辑附加公理的应用 #

公理4：若$x$不在$P$中自由出现，则$(\forall x)P\rightarrow P$

这个公理的核心作用是确保全称量词对不涉及的命题无影响，在ZFC里常用于强化公理的全局有效性。比如空集存在公理：$\exists x \forall y \neg(y \in x)$。如果我们要推导“对于任意集合$z$，空集都存在”，就可以利用这个公理：把命题$P$设为$\exists x \forall y \neg(y \in x)$，$x$不在$P$中自由出现，因此$\forall z P \rightarrow P$成立；反过来，从$P$（空集存在）就能推出$\forall z P$（任意集合旁都存在空集），保证了空集的存在性是全局成立的，不依赖于其他集合的选取。

公理5：若$P(x)$是合式公式且$t$对$x$在$P(x)$中自由，则$(\forall x)P(x)\rightarrow P(t)$

这是ZFC中最常用的代入规则，几乎所有子集构造、元素归属判断都依赖它。比如ZFC的分离公理模式：$\forall x \forall z \exists y \forall w (w \in y \leftrightarrow w \in x \land \varphi(w))$。当我们要构造具体的子集（比如集合$x$中所有偶数元素的子集）时，需要把具体元素$t$代入$w$的位置，这就用到公理5：从$\forall w (w \in y \leftrightarrow w \in x \land \varphi(w))$直接推出$t \in y \leftrightarrow t \in x \land \varphi(t)$，这是我们判断元素是否属于子集的核心逻辑。

公理6：若$P$不含$x$的自由出现，则$(\forall x)(P\rightarrow Q)\rightarrow(P\rightarrow(\forall x)Q)$

这个公理用于调整全称量词的位置，简化ZFC公理的表述和推导。比如在替换公理模式的推导中：假设我们已知“对于每个集合$x$，如果$P$（$x$上的关系是函数）成立，则$Q(x)$（存在$x$的像集）成立”，即$\forall x (P\rightarrow Q(x))$。因为$P$不涉及$x$的自由出现，利用公理6可以直接将其转换为$P\rightarrow \forall x Q(x)$——也就是“如果所有集合上的关系都是函数，那么所有集合都存在像集”，大大简化了命题的逻辑结构。

二、相等性公理的应用 #

公理7：对每个变量$x$，$x=x$

这是相等的自反性，是ZFC中证明集合唯一性的基础。比如空集的唯一性证明：假设存在两个空集$x$和$y$，根据空集定义有$\forall z \neg(z \in x)$和$\forall z \neg(z \in y)$。要应用外延公理（$\forall z (z \in x \leftrightarrow z \in y) \rightarrow x=y$），首先需要默认$x=x$、$y=y$，才能建立等价关系的前提。此外，集合运算（如交集、并集）的良定义性也依赖这个公理。

公理8：$(t_{k}=x)\rightarrow(f_{i}^{{n}(t_{1},\cdots,t_{k},\cdots,t_{n})=f_{i}}{n}(t_{1},\cdots,x,\cdots,t_{n}))$

这个公理保证函数操作对相等集合的一致性。在ZFC里，函数本质是有序对的集合，比如幂集函数$\mathcal{P}(x)$、并集函数$\bigcup x$。如果$x=y$，根据公理8，把$x$替换成$y$后，幂集的结果必然相等，即$\mathcal{P}(x)=\mathcal{P}(y)$；同理$\bigcup x=\bigcup y$。这是集合运算能成为“函数”的核心前提——输入相等则输出相等。

公理9：$(t_{k}=x)\rightarrow(A_{i}^{n}(t_{1},\cdots,t_{k},\cdots,t_{n})\rightarrow A_{i}^{n}(t_{1},\cdots,x,\cdots,t_{n}))$

这个公理是谓词的相等替换性，在ZFC里主要用于“∈”关系的一致性。比如如果$x=y$，那么对于任意$z$，$z \in x \leftrightarrow z \in y$——这是外延公理的逆命题，也是我们证明子集关系的关键：当$x=y$时，利用公理9，把$x$替换成$y$后，“$z \in x$”和“$z \in y$”的真值完全相同，因此$x \subseteq y$且$y \subseteq x$。

其实这些公理都是ZFC的“底层骨架”，平时做数学时我们不会刻意提及它们，就像走路不会刻意思考骨骼的运动，但它们确实支撑着所有集合论的表述和推导。

备注：内容来源于stack exchange，提问作者Xenomorph