Definition df-ex 1853

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 1852	. 2 wff ∃𝑥𝜑
4	1	wn 3	. . . 4 wff ¬ 𝜑
5	4, 2	wal 1629	. . 3 wff ∀𝑥 ¬ 𝜑
6	5	wn 3	. 2 wff ¬ ∀𝑥 ¬ 𝜑
7	3, 6	wb 196	1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

This definition is referenced by:  alnex  1854  eximal  1855  2nalexn  1903  2exnaln  1904  19.43OLD  1963  speimfw  2045  speimfwALT  2046  spimfw  2047  ax6ev  2059  cbvexvw  2126  hbe1w  2133  hbe1  2176  hbe1a  2177  axc16nf  2302  hbntOLD  2310  hbexOLD  2316  nfex  2318  nfexd  2329  cbvexv1  2337  ax6  2413  drex1  2477  nfexd2  2482  sbex  2611  eujustALT  2621  spcimegf  3438  spcegf  3440  spcimedv  3443  neq0f  4074  n0el  4087  dfnf5  4099  ax6vsep  4919  axnulALT  4921  axpownd  9623  gchi  9646  ballotlem2  30883  axextprim  31909  axrepprim  31910  axunprim  31911  axpowprim  31912  axinfprim  31914  axacprim  31915  distel  32038  bj-axtd  32908  bj-modald  32991  bj-modalbe  33008  bj-hbext  33031  bj-cbvexdv  33065  bj-drex1v  33078  gneispace  38951  pm10.252  39079  hbexgVD  39657  elsetrecslem  42966