such that

is always equivalent to "

is

." This is obviously extensional. It is equivalent to the assertion that the class defined by the function

is a unit class, i.e. a class having one member; in other words, a class which is a member of 1.