Definition df-ex 1781

Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1827. See also the dual pair alnex 1782 / exnal 1828. Definition of [Margaris] p. 49. (Contributed by NM, 10-Jan-1993.)

Assertion

Ref	Expression
df-ex	⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

Detailed syntax breakdown of Definition df-ex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wex 1780	. 2 wff ∃𝑥𝜑
4	1	wn 3	. . . 4 wff ¬ 𝜑
5	4, 2	wal 1539	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wn 3	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wb 206	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1782  eximal  1783  2nalexn  1829  2exnaln  1830  19.43OLD  1884  speimfw  1964  speimfwALT  1965  spimfw  1966  ax6ev  1970  cbvexvw  2038  hbe1w  2051  exexw  2054  hbe1  2146  hbe1a  2147  sbex  2283  nfex  2325  nfexd  2330  drex1v  2370  ax6  2384  drex1  2441  nfexd2  2446  eujustALT  2567  spcimegf  3504  spcegf  3542  spcimedv  3545  rexab  3649  neq0f  4295  neq0  4299  n0el  4311  abn0  4332  ax6vsep  5239  axnulALT  5240  exexneq  5375  axpownd  10492  gchi  10515  ballotlem2  34502  cbvex1v  35086  axextprim  35745  axrepprim  35746  axunprim  35747  axpowprim  35748  axinfprim  35750  axacprim  35751  distel  35845  bj-axtd  36638  bj-eximALT  36685  bj-modald  36717  bj-modalbe  36732  bj-hbext  36754  bj-cbvexdv  36844  bj-nfexd  37182  gneispace  44237  pm10.252  44464  hbexgVD  45008  elsetrecslem  49810