Axiom of extensionality (source code)

= Axiom of extensionality
{title2=$(\forall z)(z\in x\leftrightarrow z\in y)\Longrightarrow x=y$}
{wiki}

= Extensionality
{synonym}

Two <sets> with exactly the same members are equal. In a <transitive model>, all actual members of its sets are available internally, so ambient extensionality gives the internal axiom as well.