Existential quantificator vs conjunction in intuitionistic logic.

Question

It's well-know that in classical logic the following equivalence hols: $$\exists x(P\wedge Q(x))\iff P\wedge\exists xQ(x)$$ where $x$ is not free in $P$.

I ask if the same equivalence holds in intuitionistic logic. I Know that $$\exists x(P\wedge Q(x))\implies P\wedge\exists xQ(x)$$ but the only proof of reverse inclusion that i know uses contraposition.

Answer 1

The two are intuitionistically equivalent :

1) $P ∧ ∃xQ(x)$ --- premise

2) $P$ --- from 1) by ∧-elim

3) $∃xQ(x)$ --- from 1) by ∧-elim

4) $Q(x)$ --- assumed [a] from 3) for $∃$-elim

5) $P ∧ Q(x)$ --- from 2) and 4) by ∧-intro

6) $∃x(P ∧ Q(x))$ --- from 5) by $∃$-intro

7) $∃x(P ∧ Q(x))$ --- from 4)-6) by $∃$-elim, discharging assumption [a] : $x$ is not free in 7) nor in any open assumptions (i.e. into 1)).

Thus, from 1) and 7), by $\to$-intro :

$(P ∧ ∃xQ(x)) \to ∃x(P ∧ Q(x))$.