The term such that is known as an abstractor. It is used as follows, for a formula like 'x is green': |x: x is green = the x such that x is green. Likewise, one can form |x y : x loves y, which is an abstract involving a formula with two variables. And |x: x is green and |x y : x loves y are abstractions or abstracts, and are, unlike the statements or formulas they are derived from, subject terms.

In ordinary English, the respective counterparts are 'the things that are green' and 'the couples such that the first loves the second'.

The rules that are adopted for such that are often like these:

From (a1 .. an) e |x1 .. xn : F(x1 .. xn) it follows that F(a1 .. an).
From F(a1 .. an) it follows that (Ez)(z=|xi xk xm : F(a1 .. xi .. xk .. xm .. an).

Thus, one can turn from statements to abstractions and from abstractions to statements.

Since '=' is a logical connective, there often are adopted special abstractions that define some important logical constants:

Ø = |x: x≠x i.e. Ø is a symbol for the things not identical to themselves
V = |x: x=x i.e. V is a symbol for the things identical to themselves
S = |x: Fx i.e. S is a symbol for the things with property F

Normally, 'Ø' is read as 'the empty class' or 'the empty set' and 'V' as 'the universal class' or 'the universal set', on the grounds that nothing is not identical to itself, and everything is identical to itself. Of course, instead of F one can opt for other terms: "F*", "F", "S^F" etc.

This in turn allows something like a definition of the quantifiers:

(x)Fx   =def   |x:Fx = V
(Ex)Fx =def   |x:Fx ≠ Ø