From F1 <-> F2, we know that F1 and F2 are both true or both false, which in turn means $\neg F1$ has the same truth value as $\neg F2$.
By the law of noncontradiction, we have 'F1 AND (negation F1) is
unsatisfiable' and thus, 'F1 AND (negation F2) is unsatisfiable'.
By the law of Excluded Middle, we have 'F1 OR (negation F1) is valid' and thus, 'F1 OR (negation F2) is valid'.
Backward:
'F1 AND (negation F2) is unsatisfiable' means either F1 or $\neg F2$ is false. That is, $\neg F1$ or F2 is true, which is equivalent to
$F1\rightarrow F2$.
'F1 OR (negation F2) is valid' is equivalent to
$F2\rightarrow F1$.
Combine the 2 points above and you can get $F1\leftrightarrow F2$.
Yes.
Forward:
From F1 <-> F2, we know that F1 and F2 are both true or both false, which in turn means $\neg F1$ has the same truth value as $\neg F2$.
Backward:
Combine the 2 points above and you can get $F1\leftrightarrow F2$.