Definition df-ex 1780

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

This definition is referenced by:  alnex  1781  eximal  1782  2nalexn  1828  2exnaln  1829  19.43OLD  1883  speimfw  1963  speimfwALT  1964  spimfw  1965  ax6ev  1969  cbvexvw  2037  hbe1w  2049  exexw  2052  hbe1  2144  hbe1a  2145  sbex  2281  nfex  2323  nfexd  2328  drex1v  2368  ax6  2382  drex1  2439  nfexd2  2444  eujustALT  2565  spcimegf  3517  spcegf  3558  spcimedv  3561  rexab  3666  neq0f  4311  neq0  4315  n0el  4327  abn0  4348  ax6vsep  5258  axnulALT  5259  exexneq  5394  axpownd  10554  gchi  10577  ballotlem2  34480  cbvex1v  35064  axextprim  35688  axrepprim  35689  axunprim  35690  axpowprim  35691  axinfprim  35693  axacprim  35694  distel  35791  bj-axtd  36582  bj-eximALT  36629  bj-modald  36661  bj-modalbe  36676  bj-hbext  36698  bj-cbvexdv  36788  bj-nfexd  37126  gneispace  44123  pm10.252  44350  hbexgVD  44895  elsetrecslem  49685