Herbrand complexity and the epsilon calculus with equality

The e-elimination method of Hilbert's e-calculus yields the up-to-date most direct algorithm for computing the Herbrand disjunction of an extensional formula. A central advantage is that the upper bound on the Herbrand complexity obtained is independent of the propositional structure of the proof. Prior (modern) work on Hilbert's e-calculus focused mainly on the pure calculus, without equality. We clarify that this independence also holds for first-order logic with equality. Further, we provide upper bounds analyses of the extended first e-theorem, even if the formalisation incorporates so-called e-equality axioms.