Definition df-ex 1705

Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true." 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 1704	. 2 wff ∃𝑥𝜑
4	1	wn 3	. . . 4 wff ¬ 𝜑
5	4, 2	wal 1481	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wn 3	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wb 196	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1706  eximal  1707  2nalexn  1755  2exnaln  1756  19.43OLD  1811  speimfw  1876  speimfwALT  1877  spimfw  1878  ax6ev  1890  cbvexvw  1970  hbe1w  1976  hbe1  2021  hbe1a  2022  axc16nf  2137  hbntOLD  2145  hbexOLD  2152  nfex  2154  nfexd  2167  cbvexv1  2176  ax6  2251  cbvex  2272  cbvexv  2275  cbvexd  2278  drex1  2327  nfexd2  2332  sbex  2463  eujustALT  2473  spcimegf  3287  spcegf  3289  spcimedv  3292  neq0f  3926  n0fOLD  3928  n0el  3940  dfnf5  3952  ax6vsep  4785  axnulALT  4787  axpownd  9423  gchi  9446  ballotlem2  30550  axextprim  31578  axrepprim  31579  axunprim  31580  axpowprim  31581  axinfprim  31583  axacprim  31584  distel  31709  bj-axtd  32578  bj-modald  32661  bj-modalbe  32678  bj-hbext  32701  bj-cbvexdv  32736  bj-drex1v  32749  gneispace  38432  pm10.252  38560  hbexgVD  39142  elsetrecslem  42444