Description: Define a restricted class abstraction (class builder): { x e. A | ph }
is the class of all sets x in A such that ph ( x ) is true.
Definition of TakeutiZaring p. 20.

For the interpretation given in the previous paragraph to be correct, we
need to assume F/_ x A , which is the case as soon as x and A
are disjoint, which is generally the case. If A were to depend on
x , then the interpretation would be less obvious (think of the two
extreme cases A = { x } and A = x , for instance). See also
df-ral . (Contributed by NM, 22-Nov-1994)