New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ex GIF version

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
StepHypRef Expression
1 wph . . 3 wff φ
2 vx . . 3 setvar x
31, 2wex 1541 . 2 wff xφ
41wn 3 . . . 4 wff ¬ φ
54, 2wal 1540 . . 3 wff x ¬ φ
65wn 3 . 2 wff ¬ x ¬ φ
73, 6wb 176 1 wff (xφ ↔ ¬ x ¬ φ)
 Colors of variables: wff setvar class 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  2933  spcegf  2935  spcimedv  2938  n0f  3558  eq0  3564  ab0  3569
 Copyright terms: Public domain W3C validator