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

Definition df-ex 1542
Description: Define existential quantification.  E. x ph means "there exists at least one set  x such that  ph is true." Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ex  |-  ( E. x ph  <->  -.  A. x  -.  ph )

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 wph . . 3  wff  ph
2 vx . . 3  set  x
31, 2wex 1541 . 2  wff  E. x ph
41wn 3 . . . 4  wff  -.  ph
54, 2wal 1540 . . 3  wff  A. x  -.  ph
65wn 3 . 2  wff  -.  A. x  -.  ph
73, 6wb 176 1  wff  ( E. x ph  <->  -.  A. x  -.  ph )
Colors of variables: wff set 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  1752  19.8aOLD  1757  19.9ht  1779  spimehOLD  1823  hbex  1846  nfexOLD  1849  nfexd  1859  19.9tOLD  1862  equs5eOLD  1893  ax12olem5  1936  ax10  1949  a9e  1956  drex1  1972  nfexd2  1978  spime  1981  cbvex  1990  cbvexd  2014  spsbe  2080  sbex  2133  eujustALT  2212  spcimegf  2938  spcegf  2940  spcimedv  2943  n0f  3539  eq0  3545  ax9vsep  4226  axnulALT  4228  axpownd  8313  gchi  8336  xfree2  23139  nmo  23168  ballotlem2  23995  axextprim  24451  axrepprim  24452  axunprim  24453  axpowprim  24454  axinfprim  24456  axacprim  24457  distel  24718  n0el  26048  pm10.252  26879  pm10.56  26888  2exnaln  26895  hbexgVD  28444  hbexwAUX7  28872  nfexwAUX7  28874  nfexdwAUX7  28876  a9eNEW7  28893  ax10NEW7  28896  drex1NEW7  28917  spimeNEW7  28932  cbvexwAUX7  28941  spsbeNEW7  28992  sb8ewAUX7  29012  sbexNEW7  29035  hbexOLD7  29086  nfexOLD7  29089  nfexdOLD7  29092  nfexd2OLD7  29119  cbvexOLD7  29127  cbvexdOLD7  29136  sb8eOLD7  29158  ax12-2  29172  ax12-3  29173  ax12OLD  29174  a12stdy1-x12  29180  a12study9  29189  a12peros  29190  a12study5rev  29191  a12stdy1  29195  a12study  29201  a12study10  29205  a12study10n  29206  ax9lem11  29219  ax9lem12  29220  ax9lem15  29223
  Copyright terms: Public domain W3C validator