Definition df-ex 1782

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

This definition is referenced by:  alnex  1783  eximal  1784  2nalexn  1829  2exnaln  1830  19.43OLD  1884  speimfw  1966  speimfwALT  1967  spimfw  1968  ax6ev  1972  cbvexvw  2044  hbe1w  2055  hbe1  2144  hbe1a  2145  sbex  2284  nfex  2332  nfexd  2337  cbvexv1  2351  drex1v  2377  ax6  2391  drex1  2452  nfexd2  2457  eujustALT  2632  spcimegf  3537  spcegf  3539  spcimedv  3542  neq0f  4256  neq0  4259  n0el  4275  ax6vsep  5171  axnulALT  5172  axpownd  10012  gchi  10035  ballotlem2  31856  axextprim  33040  axrepprim  33041  axunprim  33042  axpowprim  33043  axinfprim  33045  axacprim  33046  distel  33161  bj-axtd  34041  bj-eximALT  34087  bj-modald  34119  bj-modalbe  34135  bj-hbext  34157  bj-cbvexdv  34237  bj-nfexd  34553  sn-dtru  39403  gneispace  40837  pm10.252  41065  hbexgVD  41612  elsetrecslem  45228