MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ex Structured version   GIF version

Definition df-ex 1552
Description: Define existential quantification. 𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true." Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ex (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 set 𝑥
31, 2wex 1551 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1550 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 178 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff set class
This definition is referenced by:  alnex  1553  2nalexn  1583  19.43OLD  1618  ax17e  1630  speimfw  1657  spimfw  1658  a9ev  1671  19.8wOLD  1708  19.9vOLD  1713  cbvexvw  1720  hbe1w  1726  hbe1  1749  excom  1759  a6e  1770  19.8aOLD  1775  hbnt  1802  19.9htOLD  1806  spimehOLD  1843  hbex  1866  nfexOLD  1869  nfexd  1876  19.9tOLD  1883  equs5eOLD  1915  ax9  1957  spimeOLD  1963  cbvex  1987  cbvexd  1992  ax12olem5OLD  2019  ax10OLD  2036  a9eOLD  2038  drex1  2063  nfexd2  2069  spsbeOLD  2153  sbex  2212  eujustALT  2291  spcimegf  3039  spcegf  3041  spcimedv  3044  n0f  3624  eq0  3630  ax9vsep  4365  axnulALT  4367  axpownd  8514  gchi  8537  xfree2  23986  ballotlem2  24781  axextprim  25185  axrepprim  25186  axunprim  25187  axpowprim  25188  axinfprim  25190  axacprim  25191  distel  25466  n0el  26820  pm10.252  27645  pm10.56  27654  2exnaln  27661  hbexgVD  29192  hbexwAUX7  29623  nfexwAUX7  29625  nfexdwAUX7  29627  a9eNEW7  29644  ax10NEW7  29647  drex1NEW7  29668  spimeNEW7  29683  cbvexwAUX7  29694  spsbeNEW7  29745  sb8ewAUX7  29768  sbexNEW7  29791  hbexOLD7  29859  nfexOLD7  29862  nfexdOLD7  29865  nfexd2OLD7  29892  cbvexOLD7  29900  cbvexdOLD7  29909  sb8eOLD7  29931
  Copyright terms: Public domain W3C validator