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 as well closed under E, 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, 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: well founded x)$$ and (2) (\forall (y,z)\in U^2: (\forall x\in y\leftrightarrow x\in z)\to \forall x\in U:(y\in x\to z\in x).