A simple FOL example in Isabelle/HOL, heavily commented :)

LogEquiv.thy

theory LogEquiv
  imports Main
begin

(* NOTATION:
   In Isabelle/HOL we write ‹(A x)› instead of ‹A(x)›
   and ‹∀x. (P x)› instead of ‹∀x: P(x)›
 *)
lemma "¬(∃x.∀y. (A x) ∧ ¬(B y)) ⟷ (∀x.∃y. (A x) ⟶ (B y))"
  by blast (* Isabelle/HOL can prove this statement automatically all by itself which proves the statement is correct. *)

(* Now let's prove it step-by-step *)
(* Essentially here we perform reasoning in an equational theory
   for the ⟷ (logical equivalence relation aka "if and only if").
   What we do is replacing (sub)formulae with equivalent ones
   until we ultimately get to a formula of a ‹P ⟷ P› shape
   which is always valid by the very definition of any equivalence
   relation (it's a mandatory reflexivity property of an equivalence
   relation along with symmetry and transitivity).
 *)
lemma "¬(∃x.∀y. (A x) ∧ ¬(B y)) ⟷ (∀x.∃y. (A x) ⟶ (B y))"
proof -
  have "(∀x.∃y. (A x) ⟶ (B y)) ⟷ (∀x.∃y. ¬(A x) ∨ (B y))" by blast (* (P ⟶ Q) ⟷ (¬P ∨ Q) *)
  also have "... ⟷ (∀x.∃y. ¬((A x) ∧ ¬(B y)))" by blast (* ¬P ∨ ¬Q ⟷ ¬(P ∧ Q) *)
  also have "... ⟷ (∀x. ¬(∀y. (A x) ∧ ¬(B y)))" by blast (* ∃x. ¬P ⟷ ¬ ∀x. P *)
  also have "... ⟷ ¬(∃x.∀y. (A x) ∧ ¬(B y))" by blast (* ∀x. ¬P ⟷ ¬ ∃x. P *)
  finally show ?thesis .. (* ‹..› to consider symmetry as I was proving in a (kinda) backwards direction *)
qed



end