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

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	wex 1528	. 2 wff E. x ph
4	1	wn 3	. . . 4 wff -. ph
5	4, 2	wal 1527	. . 3 wff A. x -. ph
6	5	wn 3	. 2 wff -. A. x -. ph
7	3, 6	wb 176	1 wff ( E. x ph <-> -. A. x -. ph )

This definition is referenced by:  alnex  1530  2nalexn  1560  19.43OLD  1593  speimfw  1626  spimfw  1627  a9ev  1637  19.8w  1659  19.9v  1663  cbvexvw  1677  hbe1w  1682  hbe1  1705  19.8a  1718  spimeh  1722  19.9ht  1726  hbex  1733  a6e  1755  nfex  1767  nfexd  1776  19.9t  1782  equs5e  1829  ax12olem5  1872  ax10  1884  a9e  1891  drex1  1907  nfexd2  1913  spime  1916  cbvex  1925  cbvexd  1949  spsbe  2015  sb8e  2033  sbex  2067  eujustALT  2146  spcimegf  2862  spcegf  2864  spcimedv  2867  n0f  3463  eq0  3469  ax9vsep  4145  axnulALT  4147  axpownd  8223  gchi  8246  xfree2  23025  ballotlem2  23047  nmo  23144  axextprim  24047  axrepprim  24048  axunprim  24049  axpowprim  24050  axinfprim  24052  axacprim  24053  distel  24160  n0el  26725  pm10.252  27556  pm10.56  27565  2exnaln  27572  hbexgVD  28682  ax12-2  29103  ax12-3  29104  ax12OLD  29105  a12stdy1-x12  29111  a12study9  29120  a12peros  29121  a12study5rev  29122  a12stdy1  29126  a12study  29132  a12study10  29136  a12study10n  29137  ax9lem11  29150  ax9lem12  29151  ax9lem15  29154