Definition df-ex 1780

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

This definition is referenced by:  alnex  1781  eximal  1782  2nalexn  1828  2exnaln  1829  19.43OLD  1883  speimfw  1963  speimfwALT  1964  spimfw  1965  ax6ev  1969  cbvexvw  2036  hbe1w  2048  exexw  2051  hbe1  2143  hbe1a  2144  sbex  2281  nfex  2324  nfexd  2329  drex1v  2374  ax6  2389  drex1  2446  nfexd2  2451  eujustALT  2572  spcimegf  3551  spcegf  3592  spcimedv  3595  rexab  3700  neq0f  4348  neq0  4352  n0el  4364  abn0  4385  ax6vsep  5303  axnulALT  5304  exexneq  5439  axpownd  10641  gchi  10664  ballotlem2  34491  cbvex1v  35088  axextprim  35701  axrepprim  35702  axunprim  35703  axpowprim  35704  axinfprim  35706  axacprim  35707  distel  35804  bj-axtd  36595  bj-eximALT  36642  bj-modald  36674  bj-modalbe  36689  bj-hbext  36711  bj-cbvexdv  36801  bj-nfexd  37139  gneispace  44147  pm10.252  44380  hbexgVD  44926  elsetrecslem  49218