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	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		wph	⊢ 𝜑
2	1 0	wex	⊢ ∃ 𝑥 𝜑
3	1	wn	⊢ ¬ 𝜑
4	3 0	wal	⊢ ∀ 𝑥 ¬ 𝜑
5	4	wn	⊢ ¬ ∀ 𝑥 ¬ 𝜑
6	2 5	wb	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )