There exists x such that P(x) and there exists x such that not P(x) implies that there exists x,y such that x does not equal to y?

Question

I'm trying to prove the following formula utilizing first order logic and natural deduction: $$\exists xP(x)\land \exists x\lnot P(x) \supset \exists xy (x\neq y) $$ So far I have tried assuming the left hand side and separating the following: $$A1 \implies \exists xP(x)\land \exists x\lnot P(x) $$ $$A1 \implies \exists xP(x)$$ $$A1 \implies \exists x\lnot P(x) $$

but I am stuck since I could not get rid of $\exists$. Am I missing something or is my way of approach wrong? Any help will be appreciated.

Edit: Available inference rules are all inference rules of the propositional logic, quantifier elimination & introduction, and substitution

Answer 1

Hint

1) $∃xP(x) ∧ ∃x¬P(x)$ --- premise

2) $∃xP(x)$ --- $∧$-elim

3) $∃x¬P(x)$ --- $∧$-elim

4) $P(a)$ --- assumed [a] from 2) for $∃$-elim

5) $¬P(b)$ --- assumed [b] from 3) for $∃$-elim

6) $\forall x \forall y (x=y)$ --- assumed [c]

7) $a=b$ --- from 6)

8) $\bot$ --- from 4), 5), 7) and $=$-elim.

Now we can discharge [a] and [b] by $∃$-elim from 2) and 3) and apply $\to$-intro with 6) to conclude with :

$¬\forall x \forall y (x=y)$.

Now, with Double Negation, we may derive : $∃x ∃y \ \lnot (x = y)$.