Can we have a theory that define small (ZFC set sizes) collections of big sets?

Question

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.

Answer 1

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.

Answer 2

Church’s Set Theory with a Universal Set, and my variant of it, though not Mitchell’s† can do some of what you ask, e.g. schema of Replacement from well founded sets, but not, I think, the set of all Frege numbers.

---

† Bibliography at “A Variant of Church’s Set Theory with a Universal Set in which the Singleton Function is a Set” (abridged), in Logique et Analyse, Vol 59, No 233 (2016) pp. 81–131. The full version is available at the Centre National de Recherches de Logique: http://www.logic-center.be/Publications/Bibliotheque/SheridanVariantChurch.pdf.