Prove $\bigcup \{A,B,C\} = (A \cup B) \cup C$

Question

Note: The analogue of this question for intersections is answered here:

Prove $\bigcap \{A,B,C\} = (A \cap B) \cap C$

This question asks how to prove $\bigcup \{A,B,C\} = (A \cup B) \cup C$. Here is my proof attempt:

\begin{align*} x \in \bigcup \{A,B,C\} &\iff \left(\exists X\right) \left(X \in \{A,B,C\} \land x \in X\right) \\ &\iff \left(\exists X\right) \left(X \in \left(\{A,B\} \cup \{C\}\right) \land x \in X\right) \\ & \quad \ \vdots \\ &\iff \left((x \in A) \lor (x \in B)\right) \lor x \in C \\ &\iff x \in (A \cup B) \lor x \in C \\ &\iff x \in (A \cup B) \cup C \end{align*}

I am not sure what formal logical results in set theory I need to fill in the intermediate steps. Especially the rigorous steps involving when the existential quantifier $\exists$ simplifies away.

Note: I know that $\cup$ is associative so I could have written $(A \cup B) \cup C$ as $A \cup (B \cup C)$, or even as "$A \cup B \cup C$", but I am trying to be as rigorous and formal as possible with logical symbols and punctuation in this proof.

Update 2015-10-18: I posted a follow-up question asking how to prove the quantification result mentioned in BrianO's answer:

Prove $∀w(∀v((v=w∧φ(v))⇔φ(w)))$

Answer 1

From some intermediate step to the conclusion: \begin{align*} x \in \bigcup \{A,B,C\} &\iff \left(\exists X \in \{A,B,C\}\right) x \in X \\ & \quad \ \vdots \\ &\iff \exists X\left( \left(\left( X = A \vee X = B \right) \vee X = C\right) \wedge x \in X \right) \\ &\iff \exists X\left( \left(\left( X = A \vee X = B \right) \wedge x \in X \right) \vee \left(X = C \wedge x \in X \right)\right)\\ &\iff \exists X\left( \left(\left( X = A \wedge x \in X \right) \vee \left(X = B \wedge x \in X \right)\right) \vee \left(X = C \wedge x \in X \right)\right)\\ &\iff \left(\exists X\left( X = A \wedge x \in X \right) \vee \exists X\left(X = B \wedge x \in X \right)\right) \vee \exists X\left(X = C \wedge x \in X \right)\\ &\iff \left((x \in A) \lor (x \in B)\right) \lor x \in C \\ &\iff x \in (A \cup B) \lor x \in C \\ &\iff x \in (A \cup B) \cup C \end{align*}

This takes a slightly different approach at the beginning.

Here's how/why you can eliminate the existential quantifier.

For a formula $\varphi$, $$\forall w \forall v((v=w \wedge \varphi(v)) \implies \varphi(w))$$

is valid and provable: it might as well be an instance of a first-order axiom schema. We assume that $v, w$ are fresh variables that don't get "captured", etc. So $v$ is not free in the consequent $\varphi(w)$, thus we can move the $v$ quantifier inside, to govern only the antecedent: $$\forall w (\exists v(v=w \wedge \varphi(v)) \implies \varphi(w))$$

So for any constant or term $t$, $$\exists v(v=t \wedge \varphi(v))⟹\varphi(t)$$ is valid and provable.

In your problem, $\varphi(v)$ is $x \in v$; you'd be taking $t$ to be $A,B,C$ in turn.

Or do it without all the formal fuss, and show that both expressions denote the same set.

Answer 2

To do any proofs, you have to define notation first. I would think that you define $$ \bigcup \{A,B,C\} = \{x | x \in A \text{ or } x \in B \text{ or } x \in C\} $$

So now, $x \in \bigcup \{A,B,C\}$ implies $x\in A$ or $x\n B$ or $x \in C$, which in turn implies $x \in A \cup B$ or $x \in C$, i.e. $x \in (A \cup B) \cup C$.

Can you go the other way?