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  2287  nfex  2328  nfexd  2333  drex1v  2373  ax6  2387  drex1  2444  nfexd2  2449  eujustALT  2571  spcimegf  3494  spcegf  3532  spcimedv  3535  rexab  3638  neq0f  4278  neq0  4282  n0el  4294  abn0  4315  ax6vsep  5227  axnulALT  5228  exexneq  5376  axpownd  10513  gchi  10536  ballotlem2  34621  cbvex1v  35204  axextprim  35871  axrepprim  35872  axunprim  35873  axpowprim  35874  axinfprim  35876  axacprim  35877  distel  35971  mh-unprimbi  36714  mh-regprimbi  36715  mh-infprim1bi  36716  mh-infprim2bi  36717  mh-infprim3bi  36718  bj-axtd  36847  bj-exim  36892  bj-modald  36956  bj-modalbe  36973  bj-cbvexdv  37095  bj-nfexd  37438  wl-eujustlem1  37901  gneispace  44549  pm10.252  44776  hbexgVD  45320  elsetrecslem  50162