Definition df-ex 1782

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 1783 / 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 1781	. 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 206	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1783  eximal  1784  2nalexn  1830  2exnaln  1831  19.43OLD  1885  speimfw  1965  speimfwALT  1966  spimfw  1967  ax6ev  1971  cbvexvw  2039  hbe1w  2052  exexw  2055  hbe1  2149  hbe1a  2150  sbex  2288  nfex  2330  nfexd  2335  drex1v  2375  ax6  2389  drex1  2446  nfexd2  2451  eujustALT  2573  spcimegf  3497  spcegf  3535  spcimedv  3538  rexab  3642  neq0f  4289  neq0  4293  n0el  4305  abn0  4326  ax6vsep  5238  axnulALT  5239  exexneq  5380  axpownd  10513  gchi  10536  ballotlem2  34639  cbvex1v  35222  axextprim  35889  axrepprim  35890  axunprim  35891  axpowprim  35892  axinfprim  35894  axacprim  35895  distel  35989  bj-axtd  36857  bj-exim  36902  bj-modald  36966  bj-modalbe  36983  bj-cbvexdv  37105  bj-nfexd  37448  wl-eujustlem1  37904  gneispace  44564  pm10.252  44791  hbexgVD  45335  elsetrecslem  50132