Theorem 19.12

Description: Theorem 19.12 of Margaris p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv and r19.12sn . (Contributed by NM, 12-Mar-1993) (Proof shortened by Wolf Lammen, 3-Jan-2018)

	Ref	Expression
Assertion	19.12	$$⊢\exists x\forall y\phi \to \forall y\exists x\phi$$

Proof

Step	Hyp	Ref	Expression
1		nfa1	$$⊢Ⅎy\forall y\phi$$
2	1	nfex	$$⊢Ⅎy\exists x\forall y\phi$$
3		sp	$$⊢\forall y\phi \to \phi$$
4	3	eximi	$$⊢\exists x\forall y\phi \to \exists x\phi$$
5	2 4	alrimi	$$⊢\exists x\forall y\phi \to \forall y\exists x\phi$$