Theorem 19.12vvv
Version of 19.12vv with a disjoint variable condition, requiring fewer
axioms. See also 19.12. (Contributed by BJ, 18-Mar-2020.)
Conclusion
\( \vdash \exists x \, \forall y \, (\varphi \rightarrow \psi) \leftrightarrow \forall y \, \exists x \, (\varphi \rightarrow \psi) \)
Proof
19.21v
l1
exbii _
\( \vdash \exists x \, \forall y \, (\varphi \rightarrow \psi) \leftrightarrow \exists x \, (\varphi \rightarrow \forall y \, \psi) \)
l2
19.36v
\( \vdash \exists x \, (\varphi \rightarrow \forall y \, \psi) \leftrightarrow \forall x \, \varphi \rightarrow \forall y \, \psi \)
19.36v
l4
albii _
\( \vdash \forall y \, \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall y \, (\forall x \, \varphi \rightarrow \psi) \)
19.21v
\( \vdash \forall y \, (\forall x \, \varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \forall y \, \psi \)
bitr2i l4 _
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \leftrightarrow \forall y \, \exists x \, (\varphi \rightarrow \psi) \)
3bitri l1 l2 _