Definition df-ex 1802

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

This definition is referenced by:  alnex  1803  eximal  1804  2nalexn  1850  2exnaln  1851  19.43OLD  1905  speimfw  1985  speimfwALT  1986  spimfw  1987  ax6ev  1991  cbvexvw  2059  hbe1w  2072  exexw  2075  hbe1  2179  hbe1a  2180  sbex  2317  nfex  2358  nfexd  2363  drex1v  2403  ax6  2417  drex1  2474  nfexd2  2479  eujustALT  2601  spcimegf  3521  spcegf  3553  spcimedv  3556  rexab  3660  neq0f  4302  neq0  4306  n0el  4319  abn0  4340  ax6vsep  5255  axnulALT  5256  exexneq  5404  axpownd  10561  gchi  10584  ballotlem2  34788  cbvex1v  35371  axextprim  36056  axrepprim  36057  axunprim  36058  axpowprim  36059  axinfprim  36061  axacprim  36062  distel  36156  mh-unprimbi  36909  mh-regprimbi  36910  mh-infprim1bi  36911  mh-infprim2bi  36912  mh-infprim3bi  36913  bj-axtd  37042  bj-exim  37087  bj-modald  37151  bj-modalbe  37168  bj-cbvexdv  37290  bj-nfexd  37633  wl-eujustlem1  38096  gneispace  44715  pm10.252  44942  hbexgVD  45486  elsetrecslem  50325