Definition df-ex 1783

Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1829. See also the dual pair alnex 1784 / exnal 1830. 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 1540	. . 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  1831  2exnaln  1832  19.43OLD  1887  speimfw  1968  speimfwALT  1969  spimfw  1970  ax6ev  1974  cbvexvw  2041  hbe1w  2052  exexw  2055  hbe1  2140  hbe1a  2141  sbex  2278  nfex  2318  nfexd  2323  drex1v  2369  ax6  2384  drex1  2441  nfexd2  2446  eujustALT  2567  spcimegf  3581  spcegf  3583  spcimedv  3586  rexab  3691  neq0f  4342  neq0  4346  n0el  4362  abn0  4381  ax6vsep  5304  axnulALT  5305  exexneq  5435  axpownd  10596  gchi  10619  ballotlem2  33487  axextprim  34670  axrepprim  34671  axunprim  34672  axpowprim  34673  axinfprim  34675  axacprim  34676  distel  34775  bj-axtd  35472  bj-eximALT  35518  bj-modald  35550  bj-modalbe  35566  bj-hbext  35588  bj-cbvexdv  35678  bj-nfexd  36019  gneispace  42885  pm10.252  43120  hbexgVD  43667  elsetrecslem  47744