Extensionality in Bernays set theory (Q1069932)

Let \(B\) be the single sorted first author theory with \(\in\), \(\sigma\) (a unary choice function symbol), \(\{\) \(x| \ldots \}\) (a term forming operator), and, as non-logical axioms, (a kind of) extensionality, choice, foundation, comprehension, and reflection. It is shown that if \(B\) proves \(\phi\), then \(B\) without extensionality proves \(\phi\) relativized to hereditarily extensional classes. This is a parallel to an old result of Gandy with Gödel-Bernays set theory instead of B.