Definition df-ex 1774

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

This definition is referenced by:  alnex  1775  eximal  1776  2nalexn  1822  2exnaln  1823  19.43OLD  1878  speimfw  1959  speimfwALT  1960  spimfw  1961  ax6ev  1965  cbvexvw  2032  hbe1w  2043  exexw  2046  hbe1  2131  hbe1a  2132  sbex  2270  nfex  2312  nfexd  2317  drex1v  2362  ax6  2377  drex1  2434  nfexd2  2439  eujustALT  2560  spcimegf  3574  spcegf  3576  spcimedv  3579  rexab  3686  neq0f  4341  neq0  4345  n0el  4361  abn0  4382  ax6vsep  5304  axnulALT  5305  exexneq  5436  axpownd  10631  gchi  10654  ballotlem2  34259  axextprim  35446  axrepprim  35447  axunprim  35448  axpowprim  35449  axinfprim  35451  axacprim  35452  distel  35550  bj-axtd  36222  bj-eximALT  36268  bj-modald  36300  bj-modalbe  36316  bj-hbext  36338  bj-cbvexdv  36428  bj-nfexd  36768  nfa1w  42240  gneispace  43711  pm10.252  43945  hbexgVD  44492  elsetrecslem  48321