Extensionality in Bernays set theory (Q1069932): Difference between revisions

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.