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  2329  nfexd  2334  drex1v  2374  ax6  2388  drex1  2445  nfexd2  2450  eujustALT  2572  spcimegf  3496  spcegf  3534  spcimedv  3537  rexab  3641  neq0f  4288  neq0  4292  n0el  4304  abn0  4325  ax6vsep  5238  axnulALT  5239  exexneq  5387  axpownd  10524  gchi  10547  ballotlem2  34633  cbvex1v  35216  axextprim  35883  axrepprim  35884  axunprim  35885  axpowprim  35886  axinfprim  35888  axacprim  35889  distel  35983  mh-unprimbi  36726  mh-regprimbi  36727  mh-infprim1bi  36728  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-axtd  36859  bj-exim  36904  bj-modald  36968  bj-modalbe  36985  bj-cbvexdv  37107  bj-nfexd  37450  wl-eujustlem1  37913  gneispace  44561  pm10.252  44788  hbexgVD  45332  elsetrecslem  50174