Definition df-ex 1783

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

This definition is referenced by:  alnex  1784  eximal  1785  2nalexn  1830  2exnaln  1831  19.43OLD  1886  speimfw  1967  speimfwALT  1968  spimfw  1969  ax6ev  1973  cbvexvw  2040  hbe1w  2051  exexw  2054  hbe1  2139  hbe1a  2140  sbex  2278  nfex  2318  nfexd  2323  drex1v  2369  ax6  2384  drex1  2441  nfexd2  2446  eujustALT  2572  spcimegf  3529  spcegf  3531  spcimedv  3534  rexab  3631  neq0f  4275  neq0  4279  n0el  4295  abn0  4314  ax6vsep  5227  axnulALT  5228  axpownd  10357  gchi  10380  ballotlem2  32455  axextprim  33642  axrepprim  33643  axunprim  33644  axpowprim  33645  axinfprim  33647  axacprim  33648  distel  33779  bj-axtd  34776  bj-eximALT  34822  bj-modald  34854  bj-modalbe  34870  bj-hbext  34892  bj-cbvexdv  34982  bj-nfexd  35309  sn-dtru  40188  gneispace  41744  pm10.252  41979  hbexgVD  42526  elsetrecslem  46404