Theorem 19.12vv

Description: 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)

	Ref	Expression
Assertion	19.12vv	$$⊢\exists x\forall y\left(\phi \to \psi \right)\leftrightarrow \forall y\exists x\left(\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.21v	$$⊢\forall y\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall y\psi \right)$$
2	1	exbii	$$⊢\exists x\forall y\left(\phi \to \psi \right)\leftrightarrow \exists x\left(\phi \to \forall y\psi \right)$$
3		nfv	$$⊢Ⅎx\psi$$
4	3	nfal	$$⊢Ⅎx\forall y\psi$$
5	4	19.36	$$⊢\exists x\left(\phi \to \forall y\psi \right)\leftrightarrow \left(\forall x\phi \to \forall y\psi \right)$$
6		19.36v	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \psi \right)$$
7	6	albii	$$⊢\forall y\exists x\left(\phi \to \psi \right)\leftrightarrow \forall y\left(\forall x\phi \to \psi \right)$$
8		nfv	$$⊢Ⅎy\phi$$
9	8	nfal	$$⊢Ⅎy\forall x\phi$$
10	9	19.21	$$⊢\forall y\left(\forall x\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \forall y\psi \right)$$
11	7 10	bitr2i	$$⊢\left(\forall x\phi \to \forall y\psi \right)\leftrightarrow \forall y\exists x\left(\phi \to \psi \right)$$
12	2 5 11	3bitri	$$⊢\exists x\forall y\left(\phi \to \psi \right)\leftrightarrow \forall y\exists x\left(\phi \to \psi \right)$$