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  3509  spcegf  3547  spcimedv  3550  rexab  3654  neq0f  4301  neq0  4305  n0el  4317  abn0  4338  ax6vsep  5249  axnulALT  5250  exexneq  5385  axpownd  10516  gchi  10539  ballotlem2  34648  cbvex1v  35232  axextprim  35897  axrepprim  35898  axunprim  35899  axpowprim  35900  axinfprim  35902  axacprim  35903  distel  35997  bj-axtd  36796  bj-eximALT  36843  bj-modald  36876  bj-modalbe  36891  bj-hbext  36913  bj-cbvexdv  37003  bj-nfexd  37345  wl-eujustlem1  37795  gneispace  44442  pm10.252  44669  hbexgVD  45213  elsetrecslem  50011