$U$ can be shown to only contain wellfounded sets by an inductive argument, given the assumption stated that replacement is obtained relative to the least class containing $U$ and $E$, and as well closed complement, intersection, domain, Cartesian product with $U$, circular permutation and transposition. There is no special assumption upon replacement here. 

Given Gandy's result in Gandy, R. [On the Axiom of Extensionality II](https://doi.org/10.2307/2963897), Journal of Symbolic Logic, 24.4, 287–300, 1959, one cannot prove the existence of non-extensional classes in $U$.

So the more comprehensive theory may safely postulate that $$(1) \ \ \forall x\in U\colon \mathrm{wellfounded}(x),$$ and $$(2) \ \ \forall (y,z)\in U^2\colon .\forall x\in U\colon(x\in y\leftrightarrow x\in z)\to \forall x\in U\colon(y\in x\to z\in x).$$