  isn’t really a formula at all, but a formula scheme, or shorthand for any of the genuine formulæ to be obtained from it by adding subscripts to ‘\(x\)’ and ‘\(y\)’. Which subscript? In every setting it will either (i) become clear which subscript, or (ii) become clear that it doesn’t matter. At all events, (A) is not an axiom of Type theory: the theory does not have a universal set, what it has is a universal set at each type.