The following FOL statement is used in my book to describe a transitive set (which ultimately sets the stage for the definition of ordinals):
$z$ is a transitive set iff $\forall y \in z [ y \subseteq z]$
Given that $y\subseteq z \leftrightarrow y \subset z \ \lor y=z $, I am a little confused as to why $y \subseteq z$ is used.
In the context of ZFC set theory, it is my understanding that $z \in z$ is always false.
Therefore if $y \in z$, then clearly $y \neq z$. So why not just use $y \subset z$?
Am I missing something? (There is clearly no logical issue either way...it just seemed odd).
Edit: After realizing that, perhaps, there are different definitions for the various symbols $\subset$, $\subseteq$, and $\subseteqq$, I figured I would add that my book (The Foundations of Mathematics by Kenneth Kunen) asserts the following definition:
$x \subseteq y \iff \forall z ( z \in x \rightarrow z \in y)$
Also, it appears as though the only two subset symbols that are used in my book are $\subseteq$ and $\subsetneqq$ (the latter has no formal definition)...there is also $\nsubseteq$, but that is obviously not applicable here.
In the presence of the axiom of foundation, it is true as you indicate that no set belongs to itself, and so the definition of transitive set can be written with $\subset$ (or $\subsetneq$, whichever symbol you prefer).
However, one may study also set theories where foundation fails, and then it is natural to define transitive sets in a way that allows self-membership. Indeed, any set $\Omega$ such that $\Omega=\{\Omega\}$, for instance, should be considered transitive.
One minor thing is that the natural translation of the natural language statement describing transitive sets gives us the rendering used by Kunen: A set $t$ is transitive if and only if any element of $t$ is a subset of $t$. This description is agnostic as to whether containment is proper or not. A somewhat more mathematical observation is that, even if Kunen is working here in a context where foundation is assumed, the definition he gives can be ported as is to a setting where foundation fails, there is no need to redefine things in this new context. This "portability" is particularly useful if one finds oneself in a situation where only fragments of ZFC hold, which is typically the case when studying independence proofs (or using countable structures in combinatorial arguments).