Definition df-ex 1812

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

This definition is used by:  alnex  1813  eximal  1814  2nalexn  1860  2exnaln  1861  19.43OLD  1915  speimfw  1995  speimfwALT  1996  spimfw  1997  ax6ev  2001  cbvexvw  2069  hbe1w  2082  exexw  2085  hbe1  2179  hbe1a  2180  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  10686  gchi  10709  ballotlem2  35163  cbvex1v  35746  axextprim  36508  axrepprim  36509  axunprim  36510  axpowprim  36511  axinfprim  36513  axacprim  36514  distel  36607  mh-unprimbi  37374  mh-regprimbi  37375  mh-infprim1bi  37376  mh-infprim2bi  37377  mh-infprim3bi  37378  bj-axtd  37506  bj-exim  37551  bj-modald  37615  bj-modalbe  37632  bj-cbvexdv  37754  bj-nfexd  38100  wl-eujustlem1  38563  gneispace  45176  pm10.252  45387  hbexgVD  45930  elsetrecslem  50834