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

Definition df-ex 1548
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 1547 . 2  wff  E. x ph
41wn 3 . . . 4  wff  -.  ph
54, 2wal 1546 . . 3  wff  A. x  -.  ph
65wn 3 . 2  wff  -.  A. x  -.  ph
73, 6wb 177 1  wff  ( E. x ph  <->  -.  A. x  -.  ph )
Colors of variables: wff set class
This definition is referenced by:  alnex  1549  2nalexn  1579  19.43OLD  1613  ax17e  1625  speimfw  1652  spimfw  1653  a9ev  1664  19.8wOLD  1701  19.9vOLD  1706  cbvexvw  1713  hbe1w  1719  hbe1  1742  excom  1752  a6e  1763  19.8aOLD  1768  hbnt  1795  19.9htOLD  1799  spimehOLD  1836  hbex  1859  nfexOLD  1862  nfexd  1869  19.9tOLD  1876  equs5eOLD  1907  ax9  1949  spimeOLD  1957  ax12olem5OLD  1981  ax10OLD  1998  a9eOLD  2000  drex1  2024  nfexd2  2030  cbvex  2038  cbvexd  2059  spsbe  2124  sbex  2178  eujustALT  2257  spcimegf  2990  spcegf  2992  spcimedv  2995  n0f  3596  eq0  3602  ax9vsep  4294  axnulALT  4296  axpownd  8432  gchi  8455  xfree2  23901  ballotlem2  24699  axextprim  25103  axrepprim  25104  axunprim  25105  axpowprim  25106  axinfprim  25108  axacprim  25109  distel  25374  n0el  26598  pm10.252  27424  pm10.56  27433  2exnaln  27440  hbexgVD  28727  hbexwAUX7  29155  nfexwAUX7  29157  nfexdwAUX7  29159  a9eNEW7  29176  ax10NEW7  29179  drex1NEW7  29200  spimeNEW7  29215  cbvexwAUX7  29224  spsbeNEW7  29275  sb8ewAUX7  29295  sbexNEW7  29318  hbexOLD7  29369  nfexOLD7  29372  nfexdOLD7  29375  nfexd2OLD7  29402  cbvexOLD7  29410  cbvexdOLD7  29419  sb8eOLD7  29441
  Copyright terms: Public domain W3C validator