Definition df-ex 1808

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

This definition is referenced by:  alnex  1809  eximal  1810  2nalexn  1856  2exnaln  1857  19.43OLD  1911  speimfw  1991  speimfwALT  1992  spimfw  1993  ax6ev  1997  cbvexvw  2065  hbe1w  2078  exexw  2081  hbe1  2176  hbe1a  2177  sbex  2314  nfex  2355  nfexd  2360  drex1v  2400  ax6  2414  drex1  2471  nfexd2  2476  eujustALT  2598  spcimegf  3518  spcegf  3550  spcimedv  3553  rexab  3657  neq0f  4301  neq0  4305  n0el  4318  abn0  4340  ax6vsep  5265  axnulALT  5266  exexneq  5416  axpownd  10585  gchi  10608  ballotlem2  34845  cbvex1v  35428  axextprim  36147  axrepprim  36148  axunprim  36149  axpowprim  36150  axinfprim  36152  axacprim  36153  distel  36247  mh-unprimbi  36999  mh-regprimbi  37000  mh-infprim1bi  37001  mh-infprim2bi  37002  mh-infprim3bi  37003  bj-axtd  37131  bj-exim  37176  bj-modald  37240  bj-modalbe  37257  bj-cbvexdv  37379  bj-nfexd  37724  wl-eujustlem1  38187  gneispace  44808  pm10.252  45019  hbexgVD  45562  elsetrecslem  50422