Is there a semantics of Set builder notation?

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?

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)$$.

• Thank you for your answer. I was able to use the fundamental property: $z \in \{ x \mid \varphi(x) \} \text { iff } \varphi (z)$ to clean out the variables and prove using the definitions that use the set builder notation. Commented May 7, 2020 at 18:16