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  3580  spcegf  3582  spcimedv  3585  rexab  3689  neq0f  4340  neq0  4344  n0el  4360  abn0  4379  ax6vsep  5302  axnulALT  5303  exexneq  5433  axpownd  10592  gchi  10615  ballotlem2  33425  axextprim  34608  axrepprim  34609  axunprim  34610  axpowprim  34611  axinfprim  34613  axacprim  34614  distel  34713  bj-axtd  35410  bj-eximALT  35456  bj-modald  35488  bj-modalbe  35504  bj-hbext  35526  bj-cbvexdv  35616  bj-nfexd  35957  gneispace  42818  pm10.252  43053  hbexgVD  43600  elsetrecslem  47646