Just a quick note, the symbol ⇔ is typically meant to stand for 'material implication' and would be better read as 'if and only if'. Or at least that is the 'no

Just a quick note, the symbol ⇔ is typically meant to stand for 'material implication' and would be better read as 'if and only if'. Or at least that is the 'normal' usage in the literature for intuitionistic logic. It doesn't really change your reading of it, but equivalent does not really capture the traditional meaning of material implication. It is more accurate to portray the logical sentence as valid with either implication in the first position. The two statements are not equivalent to each other, but the re-ordering of the implications would be, i.e. ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) is equivalent to (∀ x. (P(x) → Q)) ⇔ ((∃ x. P(x)) → Q)