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  2314  nfex  2354  nfexd  2359  drex1v  2399  ax6  2413  drex1  2470  nfexd2  2475  eujustALT  2597  spcimegf  3514  spcegf  3546  spcimedv  3549  rexab  3652  neq0f  4294  neq0  4298  n0el  4311  abn0  4333  ax6vsep  5256  axnulALT  5257  exexneq  5402  axpownd  10657  gchi  10680  ballotlem2  35055  cbvex1v  35638  axextprim  36387  axrepprim  36388  axunprim  36389  axpowprim  36390  axinfprim  36392  axacprim  36393  distel  36487  mh-unprimbi  37254  mh-regprimbi  37255  mh-infprim1bi  37256  mh-infprim2bi  37257  mh-infprim3bi  37258  bj-axtd  37386  bj-exim  37431  bj-modald  37495  bj-modalbe  37512  bj-cbvexdv  37634  bj-nfexd  37977  wl-eujustlem1  38440  gneispace  45078  pm10.252  45289  hbexgVD  45832  elsetrecslem  50714