Definition df-ex 1781

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 1782 / 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 1780	. 2 wff ∃𝑥𝜑
4	1	wn 3	. . . 4 wff ¬ 𝜑
5	4, 2	wal 1535	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wn 3	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wb 208	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1782  eximal  1783  2nalexn  1828  2exnaln  1829  19.43OLD  1884  speimfw  1966  speimfwALT  1967  spimfw  1968  ax6ev  1972  cbvexvw  2044  hbe1w  2055  hbe1  2147  hbe1a  2148  sbex  2288  nfex  2343  nfexd  2348  cbvexv1  2362  drex1v  2388  ax6  2402  drex1  2463  nfexd2  2468  eujustALT  2657  spcimegf  3589  spcegf  3591  spcimedv  3594  neq0f  4306  n0el  4321  ax6vsep  5207  axnulALT  5208  axpownd  10023  gchi  10046  ballotlem2  31746  axextprim  32927  axrepprim  32928  axunprim  32929  axpowprim  32930  axinfprim  32932  axacprim  32933  distel  33048  bj-axtd  33928  bj-eximALT  33974  bj-modald  34006  bj-modalbe  34022  bj-hbext  34044  bj-cbvexdv  34122  bj-nfexd  34433  sn-dtru  39160  gneispace  40533  pm10.252  40742  hbexgVD  41289  elsetrecslem  44850