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

Metamath Proof Explorer

Theorem 2exnexn

Description: Theorem *11.51 in WhiteheadRussell p. 164. (Contributed by Andrew Salmon, 24-May-2011) (Proof shortened by Wolf Lammen, 25-Sep-2014)

		Ref	Expression
	Assertion	2exnexn	$⊢ \exists x \forall y φ \leftrightarrow \neg \forall x \exists y \neg φ$

Step	Hyp	Ref	Expression
1		alexn	$⊢ \forall x \exists y \neg φ \leftrightarrow \neg \exists x \forall y φ$
2	1	con2bii	$⊢ \exists x \forall y φ \leftrightarrow \neg \forall x \exists y \neg φ$