Axiom of Quantifier Substitution (intuitionistic logic axiom ax-10). This is just axc11n by another name. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)