Existential quantifier proof help

Question

I know I have to use the existential elimination rule twice but I'm still having troubles.

∃x∀y((Kyf ↔ x = y) ∧ Bx), ∃x(Kxf ∧ ¬Bx) ⊢ Fa ∧ ¬Fa

Answer 1

{1}      1.   Ǝx[∀y[(Kyf ↔ x=y) & Bx]]             Prem.
{2}      2.   Ǝx[Kxf & ~Bx]                        Prem.
{3}      3.   Kbf & ~Bb                            Assum. TD(b)
{4}      4.   ∀y[(Kyf ↔ c=y) & Bc]                 Assum. TD(c)
{4}      5.   (Kbf ↔ c=b) & Bc                     4 UI
{3}      6.   Kbf                                  3 &E
{4}      7.   Kbf ↔ c=b                            5 &E
{4}      8.   (Kbf → c=b) & (c=b → Kbf)            7 ↔E
{4}      9.   Kbf → c=b                            8 &E
{3,4}    10.  c=b                                  6,9 MP
{4}      11.  Bc                                   5 &E
{3}      12.  ~Bb                                  3 &E
{3,4}    13.  ~Bc                                  10,12 =E
{14}     14.  ~(Fa & ~Fa)                          Assum
{4,14}   15.  Bc & ~(Fa & ~Fa)                     11,15 &I
{4,14}   16.  Bc                                   15 &E
{4}      17.  ~(Fa & ~Fa) → Bc                     14,16 CP
{3,4}    18.  ~~(Fa & ~Fa)                         13,17 MT
{3,4}    19.  Fa & ~Fa                             18 DNE
{1,3}    20.  Fa & ~Fa                             1,4,19 EE
{1,2}    21.  Fa & ~Fa                             2,3,20 EE

Answer 2

Here is a proof that uses explosion and a Fitch-style presentation.

The proof checker and description of inference rules can be found in the references below.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019.