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

Definition df-ex 1538
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 1537 . 2  wff  E. x ph
41wn 5 . . . 4  wff  -.  ph
54, 2wal 1532 . . 3  wff  A. x  -.  ph
65wn 5 . 2  wff  -.  A. x  -.  ph
73, 6wb 178 1  wff  ( E. x ph  <->  -.  A. x  -.  ph )
Colors of variables: wff set class
This definition is referenced by:  hbe1  1565  alnex  1569  2nalexn  1571  19.43OLD  1605  ax12o10lem4  1638  ax12o10lem8  1642  ax12o10lem12  1646  ax12olem19  1653  ax12olem25  1659  ax10  1677  a16gALT  1679  a6e  1716  nfex  1733  nfexd  1743  19.8a  1758  19.9t  1761  a9e  1817  drex1  1860  nfexd2  1866  a4ime  1869  cbvex  1878  equs5e  1913  a4sbe  1968  sb8e  1988  cbvexd  2053  sbex  2091  eujustALT  2121  cla4imegf  2837  cla4egf  2839  cla4imedv  2842  n0f  3438  eq0  3444  ax9vsep  4119  axpownd  8191  gchi  8214  xfree2  22986  ballotlem2  23009  axextprim  23420  axrepprim  23421  axunprim  23422  axpowprim  23423  axinfprim  23425  axacprim  23426  distel  23530  n0el  26093  pm10.252  26924  pm10.56  26933  2exnaln  26940  hbexgVD  27815  a4eimfK  28247  19.8vK  28254  cbvexvK  28263  hbe1wK  28267  ax12o10lem4K  28286  ax12o10lem4X  28287  ax12o10lem8K  28294  ax12o10lem8X  28295  ax12o10lem12K  28302  ax12o10lem12X  28303  ax12olem19K  28317  ax12olem19X  28318  equextvK  28323  ax12olem25X  28330  ax10X  28347  a16gALTX  28348  ax12-2  28353  ax12-3  28354  ax12OLD  28355  a12stdy1-x12  28361  a12study9  28370  a12peros  28371  a12study5rev  28372  a12stdy1  28376  a12study  28382  a12study10  28386  a12study10n  28387  ax9lem11  28400  ax9lem12  28401  ax9lem15  28404
  Copyright terms: Public domain W3C validator