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

Metamath Proof Explorer

Definition df-ex

Description: Define existential quantification. E. x ph means "there exists at least one set x such that ph is true". Dual of alex . See also the dual pair alnex / exnal . Definition of Margaris p. 49. (Contributed by NM, 10-Jan-1993)

		Ref	Expression
	Assertion	df-ex	$⊢ \exists x φ \leftrightarrow \neg \forall x \neg φ$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$setvar x$
1		wph	$wff φ$
2	1 0	wex	$wff \exists x φ$
3	1	wn	$wff \neg φ$
4	3 0	wal	$wff \forall x \neg φ$
5	4	wn	$wff \neg \forall x \neg φ$
6	2 5	wb	$wff (\exists x φ \leftrightarrow \neg \forall x \neg φ)$