This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ∃ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜑
2	1	nfex	⊢ Ⅎ 𝑦 ∃ 𝑥 ∀ 𝑦 𝜑
3		sp	⊢ ( ∀ 𝑦 𝜑 → 𝜑 )
4	3	eximi	⊢ ( ∃ 𝑥 ∀ 𝑦 𝜑 → ∃ 𝑥 𝜑 )
5	2 4	alrimi	⊢ ( ∃ 𝑥 ∀ 𝑦 𝜑 → ∀ 𝑦 ∃ 𝑥 𝜑 )