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

Definition df-ex 1531
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 1530 . 2  wff  E. x ph
41wn 3 . . . 4  wff  -.  ph
54, 2wal 1529 . . 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  1532  2nalexn  1562  19.43OLD  1595  speimfw  1628  spimfw  1629  a9ev  1639  19.8w  1661  19.9v  1665  cbvexvw  1679  hbe1w  1684  hbe1  1707  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  1909  nfexd2  1915  spime  1918  cbvex  1927  cbvexd  1951  spsbe  2017  sb8e  2035  sbex  2069  eujustALT  2148  spcimegf  2864  spcegf  2866  spcimedv  2869  n0f  3465  eq0  3471  ax9vsep  4147  axnulALT  4149  axpownd  8225  gchi  8248  xfree2  23027  ballotlem2  23049  nmo  23146  axextprim  24049  axrepprim  24050  axunprim  24051  axpowprim  24052  axinfprim  24054  axacprim  24055  distel  24162  n0el  26736  pm10.252  27567  pm10.56  27576  2exnaln  27583  hbexgVD  28755  ax12-2  29176  ax12-3  29177  ax12OLD  29178  a12stdy1-x12  29184  a12study9  29193  a12peros  29194  a12study5rev  29195  a12stdy1  29199  a12study  29205  a12study10  29209  a12study10n  29210  ax9lem11  29223  ax9lem12  29224  ax9lem15  29227
  Copyright terms: Public domain W3C validator