Definition df-ex 1778

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

This definition is referenced by:  alnex  1779  eximal  1780  2nalexn  1826  2exnaln  1827  19.43OLD  1882  speimfw  1963  speimfwALT  1964  spimfw  1965  ax6ev  1969  cbvexvw  2036  hbe1w  2048  exexw  2051  hbe1  2143  hbe1a  2144  sbex  2285  nfex  2328  nfexd  2333  drex1v  2377  ax6  2392  drex1  2449  nfexd2  2454  eujustALT  2575  spcimegf  3563  spcegf  3605  spcimedv  3608  rexab  3716  neq0f  4371  neq0  4375  n0el  4387  abn0  4408  ax6vsep  5321  axnulALT  5322  exexneq  5454  axpownd  10670  gchi  10693  ballotlem2  34453  cbvex1v  35050  axextprim  35663  axrepprim  35664  axunprim  35665  axpowprim  35666  axinfprim  35668  axacprim  35669  distel  35767  bj-axtd  36560  bj-eximALT  36607  bj-modald  36639  bj-modalbe  36654  bj-hbext  36676  bj-cbvexdv  36766  bj-nfexd  37104  gneispace  44096  pm10.252  44330  hbexgVD  44877  elsetrecslem  48791