I want to coin a theory that can speak about big sets like some of those present in NF, but at the same time comprehend over small collections of them as it is the case in ZFC. Is this known to be inconsistent. In particular I have the following system in my mind.


Have all axioms of Zermelo restricted to well founded sets only. Then add:


**Schema of Equivalence classes**
$R \text { is equivalence relation } \to \forall x \exists y (y=\{z| z \ R \ x\})$


for every *definable* relation symbol $R$ in the language of set theory.


And add:


**Schema of Universal Replacement**:
$\forall x \exists!y \phi(x,y) \land \forall y \exists!x \phi(x,y) \\\to \exists z \forall y (y \in z \leftrightarrow \exists x \phi(x,y))$


And the axiom schema of Replacement from well founded sets, i.e. only replacements of elements of well founded sets by any kind of sets is allowed. Formally this is:


**Schema of Small Replacement**:
$\forall A (A \text { is well founded } \land \forall x \in A \exists! y \phi(x,y) \\\to \exists B \forall y (y \in B \leftrightarrow \exists x \in A \phi(x,y)))$



> 
> Is there a clear inconsistency with this theory?
> 
> 
> 


This way we can speak about the set of all Frege's naturals, about any set sized collection of big sets. Also we can speak of sets of equivalence classes, like the set of all Frege numbers, which is the set of all equivalence classes with respect to bijection, so for any equivalence relation R, we can speak of the set of all equivalence classes with respect to relation R.


**[After-note]** The above question has been answered by Greg Kirmayer to be inconsistent. A possible salvage of this question would be to restrict the schema of equivalence classes to those equivalence relations that are definable after stratified formulas. 



Can we have a theory that define small (ZFC set sizes) collections of big sets?
The Schema of Equivalence classes is inconsistent with the existence of an empty set. To see this let R be the equivalence relation defined by xRy iff ((x is not in x) and (y is not in y)) or x=y. By the 
Schema of Equivalence classes {| 0} exists where 0 is empty. 


