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  1918  speimfw  1998  speimfwALT  1999  spimfw  2000  ax6ev  2004  cbvexvw  2072  hbe1w  2085  exexw  2088  hbe1  2182  hbe1a  2183  sbex  2318  nfex  2358  nfexd  2363  drex1v  2402  ax6  2416  drex1  2473  nfexd2  2478  eujustALT  2600  spcimegf  3518  spcegf  3550  spcimedv  3553  rexab  3656  neq0f  4298  neq0  4302  n0el  4315  abn0  4337  ax6vsep  5260  axnulALT  5261  exexneq  5407  axpownd  10710  gchi  10733  ballotlem2  35188  cbvex1v  35771  axextprim  36643  axrepprim  36644  axunprim  36645  axpowprim  36646  axinfprim  36648  axacprim  36649  distel  36742  mh-unprimbi  37509  mh-regprimbi  37510  mh-infprim1bi  37511  mh-infprim2bi  37512  mh-infprim3bi  37513  bj-axtd  37641  bj-exim  37686  bj-modald  37750  bj-modalbe  37767  bj-cbvexdv  37889  bj-nfexd  38248  wl-eujustlem1  38711  gneispace  45324  pm10.252  45535  hbexgVD  46077  elsetrecslem  51070