Theorem 19.12vv
Special case of 19.12 where its converse holds. See 19.12vvv for a
version with a disjoint variable condition requiring fewer axioms.
(Contributed by NM, 18-Jul-2001.) (Revised by Andrew Salmon,
11-Jul-2011.)
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) \)
nfv
nfal _
l4
19.36 _
\( \vdash \exists x \, (\varphi \rightarrow \forall y \, \psi) \leftrightarrow \forall x \, \varphi \rightarrow \forall y \, \psi \)
19.36v
l6
albii _
\( \vdash \forall y \, \exists x \, (\varphi \rightarrow \psi) \leftrightarrow \forall y \, (\forall x \, \varphi \rightarrow \psi) \)
nfv
nfal _
19.21 _
\( \vdash \forall y \, (\forall x \, \varphi \rightarrow \psi) \leftrightarrow \forall x \, \varphi \rightarrow \forall y \, \psi \)
bitr2i l6 _
\( \vdash \forall x \, \varphi \rightarrow \forall y \, \psi \leftrightarrow \forall y \, \exists x \, (\varphi \rightarrow \psi) \)
3bitri l1 l4 _