In set theory and its applications to logic, mathematics, and computer science, setbuilder notation is a mathematical notation for defining a set by stating the properties that its members must satisfy.
Setbuilder notation is be used to define a set using a predicate, that is, a logical formula that evaluates to true for each element contained in the set, and false for those elements not contained in the set.^{[1]}^{[2]} In this form, setbuilder notation has three parts: a variable, a colon or vertical bar separator, and a predicate. Thus there is a variable on the left of the separator, and a rule on the right of it. These three parts are contained in curly brackets:
or
The vertical bar (or colon) is a separator that can be read as "such that", "for which", or "with the property that". The formula Φ(x) is said to be the rule or the predicate. All values of x for which the predicate holds (is true) belong to the set being defined. All values of x for which the predicate does not hold do not belong to the set. Thus is the set of all values of x that satisfy the formula Φ.^{[3]} It may be the empty set, if no value of x satisfies the formula.
A domain E can appear on the left of the vertical bar:^{[4]}
or by adjoining it to the predicate:
The ∈ symbol here denotes set membership, while the symbol denotes the logical "and" operator, known as logical conjunction. This notation represents the set of all values of x that belong to some given set E for which the predicate is true (see "Set existence axiom" below). If is a conjunction , then is sometimes written , using a comma instead of the symbol .
In general, it is not a good idea to consider sets without defining a domain of discourse, as this would represent the subset of all possible things that may exist for which the predicate is true. This can easily lead to contradictions and paradoxes. For example, Russell's paradox shows that the expression although seemingly well formed as a set builder expression, cannot define a set without producing a contradiction.^{[5]}
In cases where the set E is clear from context, it may be not explicitly specified. It is common in the literature for an author to state the domain ahead of time, and then not specify it in the setbuilder notation. For example, an author may say something such as, "Unless otherwise stated, variables are to be taken to be natural numbers," though in less formal contexts where the domain can be assumed, a written mention is often unnecessary.
The following examples illustrate particular sets defined by setbuilder notation via predicates. In each case, the domain is specified on the left side of the vertical bar, while the rule is specified on the right side.
An extension of setbuilder notation replaces the single variable x with an expression. So instead of , we may have which should be read
For example:
When inverse functions can be explicitly stated, the expression on the left can be eliminated through simple substitution. Consider the example set . Make the substitution , which is to say , then replace t in the set builder notation to find
Two sets are equal if and only if they have the same elements. Sets defined by set builder notation are equal if and only if their set builder rules, including the domain specifiers, are equivalent. That is
if and only if
Therefore, in order to prove the equality of two sets defined by set builder notation, it suffices to prove the equivalence of their predicates, including the domain qualifiers.
For example,
because the two rule predicates are logically equivalent:
This equivalence holds because, for any real number x, we have if and only if x is a rational number with . In particular, both sets are equal to the set .
In many formal set theories, such as Zermelo–Fraenkel set theory, set builder notation is not part of the formal syntax of the theory. Instead, there is a set existence axiom scheme, which states that if E is a set and Φ(x) is a formula in the language of set theory, then there is a set Y whose members are exactly the elements of E that satisfy Φ:
The set Y obtained from this axiom is exactly the set described in set builder notation as .
Main article: List comprehension 
A similar notation available in a number of programming languages (notably Python and Haskell) is the list comprehension, which combines map and filter operations over one or more lists.
In Python, the setbuilder's braces are replaced with square brackets, parentheses, or curly braces, giving list, generator, and set objects, respectively. Python uses an Englishbased syntax. Haskell replaces the setbuilder's braces with square brackets and uses symbols, including the standard setbuilder vertical bar.
The same can be achieved in Scala using Sequence Comprehensions, where the "for" keyword returns a list of the yielded variables using the "yield" keyword.^{[6]}
Consider these setbuilder notation examples in some programming languages:
Example 1  Example 2  

Setbuilder  
Python  {l for l in L}

{(k, x) for k in K for x in X if P(x)}

Haskell  [l  l < ls]

[(k, x)  k < ks, x < xs, p x]

Scala  for (l < L) yield l

for (k < K; x < X if P(x)) yield (k,x)

C#  from l in L select l

from k in K from x in X where P(x) select (k,x)

SQL  SELECT l FROM L_set

SELECT k, x FROM K_set, X_set WHERE P(x)

Prolog  setof(L,member(L,Ls),Result)

setof((K,X),(member(K,Ks),member(X,Xs),call(P,X)),Result)

Erlang  [l  l < ls]


Julia  [l for l ∈ L]

[(k, x) for k ∈ K for x ∈ X if P(x)]

The set builder notation and list comprehension notation are both instances of a more general notation known as monad comprehensions, which permits map/filterlike operations over any monad with a zero element.