To give some context, the author (Herbert Enderton) states that:
If the following sentence is true:
$\forall t_1 ... \forall t_k$ $\exists B \forall x$ $(x \in B \iff ---)$
where '$---$' is filled with some expression involving $t_1, ... , t_k$ and $x$
Then the set B can be named by use of the abstraction notation $\{x : ---\}$
He then Extends this "abstraction notation" by way of example:
Example, to justify: $\{C-X : X \in A\}$
we must prove there is a set B such that:
$t \in B \iff t = C-X$ for some $X$ in $A$
or as another example given
to justify: $\{A \cup X : X \in B \}$
we must prove there is a set C such that:
$t \in C \iff t = A \cup X$ for some $X$ in $B$
My question is then, in a Exercise the author uses the notation:
$\{X \subseteq A : F(X) \subseteq X \}$
given the context of abstraction notation how can we justify this (it doesn't seem to follow any of the patterns for set notation that has been introduced)?
is the author simply being sloppy where the set $\{X \subseteq A : F(X) \subseteq X \}$
should really be written as $\{X : X\subseteq A \land F(X) \subseteq X\}$