Definition df-ex 1881

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

This definition is referenced by:  alnex  1882  eximal  1883  2nalexn  1928  2exnaln  1929  19.43OLD  1988  speimfw  2065  speimfwALT  2066  spimfw  2067  ax6ev  2079  cbvexvw  2146  hbe1w  2152  hbe1  2196  hbe1a  2197  axc16nf  2295  nfex  2358  nfexd  2363  cbvexv1  2370  ax6  2405  drex1  2463  nfexd2  2468  sbex  2598  eujustALT  2644  spcimegf  3505  spcegf  3507  spcimedv  3510  neq0f  4157  n0el  4170  ax6vsep  5010  axnulALT  5012  axpownd  9739  gchi  9762  ballotlem2  31097  axextprim  32123  axrepprim  32124  axunprim  32125  axpowprim  32126  axinfprim  32128  axacprim  32129  distel  32248  bj-axtd  33108  bj-modald  33197  bj-modalbe  33214  bj-hbext  33236  bj-cbvexdv  33270  bj-drex1v  33283  gneispace  39273  pm10.252  39401  hbexgVD  39961  elsetrecslem  43341