Definition df-ex 1780

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

This definition is referenced by:  alnex  1781  eximal  1782  2nalexn  1828  2exnaln  1829  19.43OLD  1883  speimfw  1963  speimfwALT  1964  spimfw  1965  ax6ev  1969  cbvexvw  2037  hbe1w  2049  exexw  2052  hbe1  2144  hbe1a  2145  sbex  2281  nfex  2323  nfexd  2328  drex1v  2368  ax6  2382  drex1  2439  nfexd2  2444  eujustALT  2565  spcimegf  3508  spcegf  3549  spcimedv  3552  rexab  3657  neq0f  4301  neq0  4305  n0el  4317  abn0  4338  ax6vsep  5245  axnulALT  5246  exexneq  5381  axpownd  10514  gchi  10537  ballotlem2  34459  cbvex1v  35043  axextprim  35676  axrepprim  35677  axunprim  35678  axpowprim  35679  axinfprim  35681  axacprim  35682  distel  35779  bj-axtd  36570  bj-eximALT  36617  bj-modald  36649  bj-modalbe  36664  bj-hbext  36686  bj-cbvexdv  36776  bj-nfexd  37114  gneispace  44110  pm10.252  44337  hbexgVD  44882  elsetrecslem  49688