Definition df-ex 1782

Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1828. See also the dual pair alnex 1783 / exnal 1829. 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 1781	. 2 wff ∃𝑥𝜑
4	1	wn 3	. . . 4 wff ¬ 𝜑
5	4, 2	wal 1540	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wn 3	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wb 206	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1783  eximal  1784  2nalexn  1830  2exnaln  1831  19.43OLD  1885  speimfw  1965  speimfwALT  1966  spimfw  1967  ax6ev  1971  cbvexvw  2039  hbe1w  2052  exexw  2055  hbe1  2149  hbe1a  2150  sbex  2288  nfex  2330  nfexd  2335  drex1v  2375  ax6  2389  drex1  2446  nfexd2  2451  eujustALT  2573  spcimegf  3497  spcegf  3535  spcimedv  3538  rexab  3642  neq0f  4289  neq0  4293  n0el  4305  abn0  4326  ax6vsep  5239  axnulALT  5240  exexneq  5386  axpownd  10521  gchi  10544  ballotlem2  34630  cbvex1v  35213  axextprim  35880  axrepprim  35881  axunprim  35882  axpowprim  35883  axinfprim  35885  axacprim  35886  distel  35980  mh-unprimbi  36723  mh-regprimbi  36724  mh-infprim1bi  36725  mh-infprim2bi  36726  mh-infprim3bi  36727  bj-axtd  36856  bj-exim  36901  bj-modald  36965  bj-modalbe  36982  bj-cbvexdv  37104  bj-nfexd  37447  wl-eujustlem1  37910  gneispace  44558  pm10.252  44785  hbexgVD  45329  elsetrecslem  50165