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

Definition df-ex 1558
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 1557 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1556 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 178 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff set class
This definition is referenced by:  alnex  1559  2nalexn  1590  2exnaln  1591  19.43OLD  1626  ax17e  1638  speimfw  1665  spimfw  1666  a9ev  1679  19.8wOLD  1714  19.9vOLD  1719  cbvexvw  1726  hbe1w  1732  hbe1  1755  excom  1765  a6e  1776  19.8aOLD  1782  hbnt  1809  19.9htOLD  1813  spimehOLD  1851  hbex  1874  nfexOLD  1877  nfexd  1884  19.9tOLD  1891  equs5eOLD  1923  ax9  1968  spimeOLD  1974  cbvex  1998  cbvexd  2003  ax12olem5OLD  2029  ax10OLD  2045  a9eOLD  2047  drex1  2075  nfexd2  2081  spsbeOLD  2164  sbex  2242  eujustALT  2324  spcimegf  3077  spcegf  3079  spcimedv  3082  n0f  3665  eq0  3671  ax9vsep  4418  axnulALT  4420  axpownd  8573  gchi  8596  xfree2  24080  ballotlem2  25139  axextprim  25610  axrepprim  25611  axunprim  25612  axpowprim  25613  axinfprim  25615  axacprim  25616  distel  25888  n0el  27232  pm10.252  28055  pm10.56  28064  hbexgVD  29986  hbexwAUX7  30499  nfexwAUX7  30501  nfexdwAUX7  30503  a9eNEW7  30520  ax10NEW7  30523  drex1NEW7  30544  spimeNEW7  30559  cbvexwAUX7  30570  spsbeNEW7  30621  sb8ewAUX7  30644  sbexNEW7  30667  hbexOLD7  30735  nfexOLD7  30738  nfexdOLD7  30741  nfexd2OLD7  30768  cbvexOLD7  30776  cbvexdOLD7  30785  sb8eOLD7  30807
  Copyright terms: Public domain W3C validator