Existential Quantifier Distributes over Conjunction

Theorem

Let $\map \phi x, \map \psi x$ be WFFs of the free variable $x$.

Then:

$\exists x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$

Proof

By the tableau method of natural deduction:

$\exists x: \paren {\map \phi x \land \map \psi x} \vdash \paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$
Line Pool Formula Rule Depends upon Notes
1 1 $\exists x: \paren {\map \phi x \land \map \psi x}$ Premise
2 2 $\map \phi {x \gets x_0} \land \map \psi {x \gets x_0}$ Assumption $x_0$ is arbitrary
3 2 $\map \phi {x \gets x_0}$ Rule of Simplification 2
4 2 $\exists x: \map \phi x$ Existential Generalisation 3
5 2 $\map \psi {x \gets x_0}$ Rule of Simplification 2
6 2 $\exists x: \map \psi x$ Existential Generalisation 5
7 2 $\paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$ Rule of Conjunction 4, 6
8 1 $\paren {\exists x: \map \phi x} \land \paren {\exists x: \map \psi x}$ Existential Instantiation 1, 2-7

$\blacksquare$