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  1859  nfexd2  1865  a4ime  1868  cbvex  1877  equs5e  1912  a4sbe  1967  sb8e  1987  cbvexd  2052  sbex  2088  eujustALT  2117  cla4imegf  2800  cla4egf  2802  cla4imedv  2804  n0f  3370  eq0  3376  ax9vsep  4042  axpownd  8103  gchi  8126  xfree2  22855  axextprim  23218  axrepprim  23219  axunprim  23220  axpowprim  23221  axinfprim  23223  axacprim  23224  distel  23328  n0el  25891  pm10.252  26722  pm10.56  26731  2exnaln  26738  hbexgVD  27372  ax12-2  27792  ax12-3  27793  ax12OLD  27794  a12stdy1-x12  27800  a12study9  27809  a12peros  27810  a12study5rev  27811  a12stdy1  27815  a12study  27821  a12study10  27825  a12study10n  27826  ax9lem11  27839  ax9lem12  27840  ax9lem15  27843
  Copyright terms: Public domain W3C validator