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

Definition df-ex 1529
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 1528 . 2  wff  E. x ph
41wn 3 . . . 4  wff  -.  ph
54, 2wal 1527 . . 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  1530  2nalexn  1560  19.43OLD  1593  speimfw  1626  spimfw  1627  a9ev  1638  19.8w  1660  19.9v  1664  cbvexvw  1678  hbe1w  1683  hbe1  1706  19.8a  1720  spimeh  1724  19.9ht  1728  hbex  1735  a6e  1757  nfex  1769  nfexd  1778  19.9t  1784  equs5e  1831  ax12olem5  1874  ax10  1886  a9e  1893  drex1  1910  nfexd2  1916  spime  1919  cbvex  1928  cbvexd  1954  spsbe  2014  sb8e  2032  sbex  2070  eujustALT  2147  spcimegf  2863  spcegf  2865  spcimedv  2868  n0f  3464  eq0  3470  ax9vsep  4146  axpownd  8219  gchi  8242  xfree2  23021  ballotlem2  23043  axextprim  23454  axrepprim  23455  axunprim  23456  axpowprim  23457  axinfprim  23459  axacprim  23460  distel  23564  n0el  26136  pm10.252  26967  pm10.56  26976  2exnaln  26983  hbexgVD  27962  ax12-2  28382  ax12-3  28383  ax12OLD  28384  a12stdy1-x12  28390  a12study9  28399  a12peros  28400  a12study5rev  28401  a12stdy1  28405  a12study  28411  a12study10  28415  a12study10n  28416  ax9lem11  28429  ax9lem12  28430  ax9lem15  28433
  Copyright terms: Public domain W3C validator