User:Dfeuer/Set Difference of Universal Class and Non-Empty Set is not Transitive

Theorem

Let $\mathbb U$ be the universal class.

Let $y$ be a non-empty set.

Then the set difference $\mathbb U \setminus y$ is not transitive.

Proof

Since $y ≠ \varnothing$ there is an $x \in y$.

By the Dfeuer/Axiom Schema of Separation there is a class $C$ consisting of precisely those sets that contain $x$.

By User:Dfeuer/Class of Supersets is not Set, $C$ is not a set.

Since User:Dfeuer/Subclass of Set is Set, $C \not\subseteq y$.

Thus there is some $z \in C$ such that $z \notin y$.

By the definition of $C$, $x \in z$.

Since $z \notin y$, $z \in \mathbb U \setminus y$.

So $x \in z$, $z \in \mathbb U \setminus y$, but $x \notin \mathbb U \setminus y$, so $\mathbb U \setminus y$ is not transitive.