Definition df-ex 1776

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

This definition is referenced by:  alnex  1777  eximal  1778  2nalexn  1824  2exnaln  1825  19.43OLD  1880  speimfw  1960  speimfwALT  1961  spimfw  1962  ax6ev  1966  cbvexvw  2033  hbe1w  2045  exexw  2048  hbe1  2140  hbe1a  2141  sbex  2279  nfex  2322  nfexd  2327  drex1v  2371  ax6  2386  drex1  2443  nfexd2  2448  eujustALT  2569  spcimegf  3550  spcegf  3591  spcimedv  3594  rexab  3702  neq0f  4353  neq0  4357  n0el  4369  abn0  4390  ax6vsep  5308  axnulALT  5309  exexneq  5444  axpownd  10638  gchi  10661  ballotlem2  34469  cbvex1v  35066  axextprim  35680  axrepprim  35681  axunprim  35682  axpowprim  35683  axinfprim  35685  axacprim  35686  distel  35784  bj-axtd  36576  bj-eximALT  36623  bj-modald  36655  bj-modalbe  36670  bj-hbext  36692  bj-cbvexdv  36782  bj-nfexd  37120  gneispace  44123  pm10.252  44356  hbexgVD  44903  elsetrecslem  48929