Definition df-ex 1788

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

This definition is referenced by:  alnex  1789  eximal  1790  2nalexn  1836  2exnaln  1837  19.43OLD  1891  speimfw  1971  speimfwALT  1972  spimfw  1973  ax6ev  1977  cbvexvw  2045  hbe1w  2058  exexw  2061  hbe1  2156  hbe1a  2157  sbex  2294  nfex  2335  nfexd  2340  drex1v  2380  ax6  2394  drex1  2451  nfexd2  2456  eujustALT  2578  spcimegf  3498  spcegf  3531  spcimedv  3534  rexab  3637  neq0f  4278  neq0  4282  n0el  4294  abn0  4315  ax6vsep  5227  axnulALT  5228  exexneq  5376  axpownd  10520  gchi  10543  ballotlem2  34683  cbvex1v  35269  axextprim  35942  axrepprim  35943  axunprim  35944  axpowprim  35945  axinfprim  35947  axacprim  35948  distel  36042  mh-unprimbi  36785  mh-regprimbi  36786  mh-infprim1bi  36787  mh-infprim2bi  36788  mh-infprim3bi  36789  bj-axtd  36918  bj-exim  36963  bj-modald  37027  bj-modalbe  37044  bj-cbvexdv  37166  bj-nfexd  37509  wl-eujustlem1  37972  gneispace  44591  pm10.252  44818  hbexgVD  45362  elsetrecslem  50201