I know that $\alpha \Leftrightarrow \beta$ is equivalent to $(\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \alpha)$.
I want to expand the biconditional in $\forall x\exists y \text{ Qt}(x) \Leftrightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right)$ to two implications (with the end goal being to convert it to conjunctive normal form).
What happens to the quantifiers when the biconditional is expanded?
Does $\forall x \exists y$ stay with $\text{Qt}(x)$, as in $\left( \left( \forall x\exists y \text{ Qt}(x) \right) \Rightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \right) \wedge \left( \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \Rightarrow \left( \forall x\exists y \text{ Qt}(x) \right) \right)$?
Or does it stay on the left side of each implication, as in $\left( \left( \forall x\exists y \text{ Qt}(x) \right) \Rightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \right) \wedge \left( \left( \forall x\exists y \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \right) \Rightarrow \text{ Qt}(x) \right)$?
Neither?
You have $$ \forall x\exists y \text{ Qt}(x) \Leftrightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \text{,} $$ but what you really have is $$ \forall x\exists y \bigg( \text{ Qt}(x) \Leftrightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \bigg) \text{.} $$ The quantifiers bind the variables $x$ and $y$. This means the quantifiers extend to the end of the binding. Note that $x$ and $y$ are use on the right of the biimplication, so the quantified expression includes "$\left( \text{Pr}(x) \wedge \text{Sr}(y) \right)$".
Then $$ \forall x\exists y \text{ Qt}(x) \Leftrightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) $$ becomes $$ \forall x\exists y \bigg( \big( \text{ Qt}(x) \Rightarrow \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \big) \wedge \big( \left( \text{Pr}(x) \wedge \text{Sr}(y) \right) \Rightarrow \text{ Qt}(x) \big) \bigg) \text{.} $$