Is there a semantics of Set builder notation?

Question

I'm doing a very simple proof to show the following distributive property:

$$A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$$

The website proofwiki argues as follows:

$\displaystyle$ $x \in A \cap (A \cup B)$

$\iff$ {Definition of Set Union and Definition of Set Intersection}

$\displaystyle x \in A \land (x \in B \lor x \in C)$

$\iff$ {Conjunction is Left Distributive over Disjunction}

$\displaystyle (x \in A \land x \in B) \lor (x \in A \land x \in C)$

$\iff$ {Definition of Set Union and Definition of Set Intersection}

$\displaystyle x \in (A \cap B \cup (A \cap C)$

$\blacksquare$

The rewrites for the definitions they use are simply:

$x \in A \cup B \iff x \in A \lor x \in B$

$x \in A \cap B \iff x \in A \land x \in B$

---

My Problem

I think those definitions are a little informal and I wish to use the Set Builder notation for defining my sets properly:

$A \cup B = \{x: x \in A \lor x \in B\}$

$A \cap B = \{x: x \in A \land x \in B\}$

The use of these definitions cause problems in my proof because I need some semantics or some theorems on set builder notation to shuffle the symbols:

$\{x: x \in A \cap ( B \cup C)\}$

$\iff$ {My Definition of Set Intersection}

$\{x: x \in \{y: y \in A \land y \in (B \cup C) \} \}$

$\iff$ {My Definition of Set Union}

$\{x: x \in \{y: y \in A \land y \in \{z: z \in B \lor z \in C\} \}$

This part is confusing because I don't have any useful lemma/theorem to rewrite the variables that bind the inner sets using the variable in the outer scope. (like Lambda calculus has α-conversion, β-reduction)

My question: How can I get the semantics of this language of set builders so that I can rewrite the above statement where I can distribute the conjunction and how can I then re-use my definitions to get to the RHS?

Answer 1

The set-builder notation is an "operator" that has as input a formula and outputs a term (a "name").

The meaning of $\{ x \mid \varphi(x) \}$ is:

the set of all and only those objects that satisfy the "condition" expressed by formula $\varphi$ [see the examples above with $A \cup B$ and $A \cap B$].

The fundamental property of the notation is:

$z \in \{ x \mid \varphi(x) \} \text { iff } \varphi (z)$.

---

What does it mean in terms of your problem ?

That $\{ x \mid x \in A \cap (B \cup C) \} = \{ x \mid x \in A \text { and } (x \in B \text { or } x \in C)\}$.

The formula $\varphi(x)$ used to "specify" the condition inside the set-builder notation is:

$x \in A \text { and } (x \in B \text { or } x \in C)$

and you can work on it using distributivity trasforming it into the equivalent : $(x \in A \text { and } x \in B) \text { or } (x \in A \text { and } x \in C)$.