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  2036  hbe1w  2048  exexw  2051  hbe1  2143  hbe1a  2144  sbex  2281  nfex  2324  nfexd  2329  drex1v  2373  ax6  2388  drex1  2445  nfexd2  2450  eujustALT  2571  spcimegf  3530  spcegf  3571  spcimedv  3574  rexab  3678  neq0f  4323  neq0  4327  n0el  4339  abn0  4360  ax6vsep  5273  axnulALT  5274  exexneq  5409  axpownd  10613  gchi  10636  ballotlem2  34467  cbvex1v  35051  axextprim  35664  axrepprim  35665  axunprim  35666  axpowprim  35667  axinfprim  35669  axacprim  35670  distel  35767  bj-axtd  36558  bj-eximALT  36605  bj-modald  36637  bj-modalbe  36652  bj-hbext  36674  bj-cbvexdv  36764  bj-nfexd  37102  gneispace  44105  pm10.252  44333  hbexgVD  44878  elsetrecslem  49511