Axiom of Extensionality - in Set Theory With Ur-elements

In Set Theory With Ur-elements

An ur-element is a member of a set that is not itself a set. In the Zermelo–Fraenkel axioms, there are no ur-elements, but they are included in some alternative axiomatisations of set theory. Ur-elements can be treated as a different logical type from sets; in this case, makes no sense if is an ur-element, so the axiom of extensionality simply applies only to sets.

Alternatively, in untyped logic, we can require to be false whenever is an ur-element. In this case, the usual axiom of extensionality would then imply that every ur-element is equal to the empty set. To avoid this consequence, we can modify the axiom of extensionality to apply only to nonempty sets, so that it reads:

That is:

Given any set A and any set B, if A is a nonempty set (that is, if there exists a member C of A), then if A and B have precisely the same members, then they are equal.

Yet another alternative in untyped logic is to define itself to be the only element of whenever is an ur-element. While this approach can serve to preserve the axiom of extensionality, the axiom of regularity will need an adjustment instead.