Definition df-ex 1788

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

This definition is referenced by:  alnex  1789  eximal  1790  2nalexn  1835  2exnaln  1836  19.43OLD  1891  speimfw  1972  speimfwALT  1973  spimfw  1974  ax6ev  1978  cbvexvw  2045  hbe1w  2056  exexw  2059  hbe1  2145  hbe1a  2146  sbex  2284  nfex  2325  nfexd  2330  drex1v  2371  ax6  2385  drex1  2442  nfexd2  2447  eujustALT  2573  spcimegf  3520  spcegf  3522  spcimedv  3525  rexab  3625  neq0f  4273  neq0  4277  n0el  4293  abn0  4312  ax6vsep  5220  axnulALT  5221  axpownd  10263  gchi  10286  ballotlem2  32330  axextprim  33517  axrepprim  33518  axunprim  33519  axpowprim  33520  axinfprim  33522  axacprim  33523  distel  33660  bj-axtd  34678  bj-eximALT  34724  bj-modald  34756  bj-modalbe  34772  bj-hbext  34794  bj-cbvexdv  34884  bj-nfexd  35212  sn-dtru  40088  gneispace  41606  pm10.252  41841  hbexgVD  42388  elsetrecslem  46263