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  2120  cla4imegf  2813  cla4egf  2815  cla4imedv  2818  n0f  3405  eq0  3411  ax9vsep  4085  axpownd  8156  gchi  8179  xfree2  22950  ballotlem2  22973  axextprim  23384  axrepprim  23385  axunprim  23386  axpowprim  23387  axinfprim  23389  axacprim  23390  distel  23494  n0el  26057  pm10.252  26888  pm10.56  26897  2exnaln  26904  hbexgVD  27695  a4eimfK  28127  19.8vK  28134  cbvexvK  28143  hbe1wK  28147  ax12o10lem4K  28166  ax12o10lem4X  28167  ax12o10lem8K  28174  ax12o10lem8X  28175  ax12o10lem12K  28182  ax12o10lem12X  28183  ax12olem19K  28197  ax12olem19X  28198  equextvK  28203  ax12olem25X  28210  ax10X  28227  a16gALTX  28228  ax12-2  28233  ax12-3  28234  ax12OLD  28235  a12stdy1-x12  28241  a12study9  28250  a12peros  28251  a12study5rev  28252  a12stdy1  28256  a12study  28262  a12study10  28266  a12study10n  28267  ax9lem11  28280  ax9lem12  28281  ax9lem15  28284
  Copyright terms: Public domain W3C validator