Definition df-ex 1813

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

This definition is used by:  alnex  1814  eximal  1815  2nalexn  1861  2exnaln  1862  19.43OLD  1916  speimfw  1996  speimfwALT  1997  spimfw  1998  ax6ev  2002  cbvexvw  2070  hbe1w  2083  exexw  2086  hbe1  2180  hbe1a  2181  sbex  2316  nfex  2356  nfexd  2361  drex1v  2401  ax6  2415  drex1  2472  nfexd2  2477  eujustALT  2599  spcimegf  3517  spcegf  3549  spcimedv  3552  rexab  3656  neq0f  4298  neq0  4302  n0el  4315  abn0  4337  ax6vsep  5264  axnulALT  5265  exexneq  5414  axpownd  10611  gchi  10634  ballotlem2  34985  cbvex1v  35568  axextprim  36265  axrepprim  36266  axunprim  36267  axpowprim  36268  axinfprim  36270  axacprim  36271  distel  36365  mh-unprimbi  37148  mh-regprimbi  37149  mh-infprim1bi  37150  mh-infprim2bi  37151  mh-infprim3bi  37152  bj-axtd  37280  bj-exim  37325  bj-modald  37389  bj-modalbe  37406  bj-cbvexdv  37528  bj-nfexd  37873  wl-eujustlem1  38336  gneispace  44959  pm10.252  45170  hbexgVD  45713  elsetrecslem  50610