Collection is not provable in ZFC minus extensionality, a simple countermodel is described in http://mathoverflow.net/questions/54328 . (That the model cannot provably satisfy collection follows from Gödel’s theorem. For a specific instance of collection which fails, let $\bar\omega$ denote one of the many representations of $\omega$ in the model, and $\bar0\in\bar\omega$ the corresponding empty set: then the model satisfies “for every $n\in\bar\omega\smallsetminus\{\bar0\}$, there exists a well-order of type function $\omega+n$” for every f$with domain$n\in\bar\omega$, n$ such that $f(\bar0)=\bar\omega$, and $f(x)\in f(y)$ whenever $x\in y\in n$”, but there is no set collecting such well-orders functions for every $n\in\bar\omega$. A little care is needed to express this sensibly without extensionality.)n\in\bar\omega\smallsetminus\{\bar0\}$.) 2 added 468 characters in body Collection is not provable in ZFC minus extensionality, a simple countermodel is described in http://mathoverflow.net/questions/54328 . (That the model cannot provably satisfy collection follows from Gödel’s theorem. For a specific instance of collection which fails, let$\bar\omega$denote one of the many representations of$\omega$in the model: then the model satisfies there exists a well-order of type$\omega+n$” for every$n\in\bar\omega$, but there is no set collecting such well-orders for every$n\in\bar\omega\$. A little care is needed to express this sensibly without extensionality.)