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\phi \leftrightarrow \neg \forall x\neg \phi$$

Detailed syntax breakdown

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