En ZFC con términos de clase, una clase es simplemente un predicado unario $\varphi$ del lenguaje que luego escribimos como
$$\{X\mid\varphi(X)\}$$
lo cual solo sugiere que hemos construido una colección de estos objetos. Escribimos $Y\in\{X\mid \varphi(X)\}$ para $\varphi(Y)$. Además, decimos que tal clase (término) $\mathcal C$ es un conjunto si
$$\exists X\forall Y[Y\in X\leftrightarrow Y\in\mathcal C].$$
En NBG y teorías de conjuntos similares (que se basan en clases en lugar de conjuntos) cada conjunto también es una clase. ¿Pero esto es cierto para este enfoque de ZFC? Para mí parece que una clase es solo una fórmula. Y hay conjuntos que no puedo describir completamente usando tal fórmula, por ejemplo, un conjunto dado por el axioma de elección.
¿Son los conjuntos y las clases en ZFC (con términos de clase) simplemente conceptos diferentes, cada uno no siendo un "sub-concepto" del otro?
Después de la respuesta de Asaf:
No me siento muy bien al escribir $\{X\mid X\in A\}$ para conjuntos arbitrarios $A$ porque para mí $A$ no es un símbolo del lenguaje. Sin embargo, cuando mi conjunto $A$ es definible por un predicado $\varphi$ con
$$\mathrm{ZFC}\vdash \exists A \varphi(A) \quad\text{ and }\quad \mathrm{ZFC}\vdash\varphi(A)\wedge \varphi(B)\to A=B,$$
entonces podría escribir $\{X\mid \forall A[\varphi(A)\to X\in A]\}$, y esto se sentiría bien. Pero mi problema son los conjuntos para los cuales no existe tal $\varphi$. No sé cómo puedo incluir tal noción abreviada (como $\{X\mid X\in A\}$) en una prueba formal sin sentirme completamente seguro de lo que realmente estoy haciendo.
