natural deduction with two quantifiers on both sides of the double implication

Question

I need help to understand step by step of the follow natural deduction

∃x∀y ¬α(x, y) ↔ ¬∀x∃y α(x, y)

I'm used to making natural deductions, but in this case they have two quantifiers on each side and I'm a little confused by the rules to apply

I would like to know how to proceed with the ∃ exclusion rules in this example.

Below are the last lines to explain the format of natural deduction i'm making.

          [∃x∀y ¬α(x, y)]                         [¬∀x∃y α(x, y)]            
                 ...                                      ...
           ¬∀x∃y α(x, y)                             ∃x∀y ¬α(x, y)
___________________________________I➔    ___________________________________I➔
    ∃x∀y ¬α(x, y) ➔ ¬∀x∃y α(x, y)          ¬∀x∃y α(x, y) ➔ ∃x∀y ¬α(x, y)
____________________________________________________________________________I↔
                        ∃x∀y ¬α(x, y) ↔ ¬∀x∃y α(x, y)

Answer 1

Using a form of natural deduction (screenshot from my proof checker)

Now, do it backwards to obtain the biconditional.