Definition df-ex 1782

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

This definition is referenced by:  alnex  1783  eximal  1784  2nalexn  1830  2exnaln  1831  19.43OLD  1885  speimfw  1965  speimfwALT  1966  spimfw  1967  ax6ev  1971  cbvexvw  2039  hbe1w  2052  exexw  2055  hbe1  2149  hbe1a  2150  sbex  2286  nfex  2328  nfexd  2333  drex1v  2373  ax6  2387  drex1  2444  nfexd2  2449  eujustALT  2571  spcimegf  3507  spcegf  3545  spcimedv  3548  rexab  3652  neq0f  4299  neq0  4303  n0el  4315  abn0  4336  ax6vsep  5247  axnulALT  5248  exexneq  5383  axpownd  10514  gchi  10537  ballotlem2  34625  cbvex1v  35209  axextprim  35874  axrepprim  35875  axunprim  35876  axpowprim  35877  axinfprim  35879  axacprim  35880  distel  35974  bj-axtd  36767  bj-eximALT  36814  bj-modald  36847  bj-modalbe  36862  bj-hbext  36884  bj-cbvexdv  36974  bj-nfexd  37312  wl-eujustlem1  37762  gneispace  44412  pm10.252  44639  hbexgVD  45183  elsetrecslem  49981