 (A\(4')\), like (A4), restricts specification to objects within \(\bD\), but it uses a quantifier instead of ‘\(\rE!\)’ to do so. The quantifier permutation axiom (A\(5')\) is redundant in the presence of the identity axioms but, as Fine proved in (1983), is independent of the other axioms.