换名规则

设 $A$ 为一公式, 将 $A$ 中某量词辖域中个体变项的所有约束出现以及相应的指导变元换成下雨中未出现的个体变项, 所得公式为 $A^{\prime }$, 则 $A^{\prime }\iff A$.