Definition df-ex 1542

Description: Define existential quantification. ∃xφ means "there exists at least one set x such that φ is true." Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-ex	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)

Detailed syntax breakdown of Definition df-ex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3	1, 2	wex 1541	. 2 wff ∃xφ
4	1	wn 3	. . . 4 wff ¬ φ
5	4, 2	wal 1540	. . 3 wff ∀x ¬ φ
6	5	wn 3	. 2 wff ¬ ∀x ¬ φ
7	3, 6	wb 176	1 wff (∃xφ ↔ ¬ ∀x ¬ φ)

This definition is referenced by:  alnex  1543  2nalexn  1573  19.43OLD  1606  ax17e  1618  speimfw  1645  spimfw  1646  a9ev  1656  19.8wOLD  1693  19.9vOLD  1697  cbvexvw  1703  hbe1w  1708  hbe1  1731  excom  1741  a6e  1751  19.8a  1756  19.9ht  1778  spimehOLD  1821  hbex  1841  nfexOLD  1844  nfexd  1854  19.9tOLD  1857  equs5e  1888  ax12olem5  1931  ax10  1944  a9e  1951  drex1  1967  nfexd2  1973  spime  1976  cbvex  1985  cbvexd  2009  spsbe  2075  sb8e  2093  sbex  2128  eujustALT  2207  spcimegf  2934  spcegf  2936  spcimedv  2939  n0f  3559  eq0  3565  ab0  3570