Definition df-ex 1551

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 1550	. 2 wff E. x ph
4	1	wn 3	. . . 4 wff -. ph
5	4, 2	wal 1549	. . 3 wff A. x -. ph
6	5	wn 3	. 2 wff -. A. x -. ph
7	3, 6	wb 177	1 wff ( E. x ph <-> -. A. x -. ph )

This definition is referenced by:  alnex  1552  2nalexn  1582  19.43OLD  1616  ax17e  1628  speimfw  1655  spimfw  1656  a9ev  1668  19.8wOLD  1705  19.9vOLD  1710  cbvexvw  1717  hbe1w  1723  hbe1  1746  excom  1756  a6e  1767  19.8aOLD  1772  hbnt  1799  19.9htOLD  1803  spimehOLD  1840  hbex  1863  nfexOLD  1866  nfexd  1873  19.9tOLD  1880  equs5eOLD  1911  ax9  1953  spimeOLD  1959  cbvex  1983  cbvexd  1988  ax12olem5OLD  2015  ax10OLD  2032  a9eOLD  2034  drex1  2055  nfexd2  2061  spsbeOLD  2149  sbex  2204  eujustALT  2283  spcimegf  3022  spcegf  3024  spcimedv  3027  n0f  3628  eq0  3634  ax9vsep  4326  axnulALT  4328  axpownd  8468  gchi  8491  xfree2  23940  ballotlem2  24738  axextprim  25142  axrepprim  25143  axunprim  25144  axpowprim  25145  axinfprim  25147  axacprim  25148  distel  25423  n0el  26689  pm10.252  27514  pm10.56  27523  2exnaln  27530  hbexgVD  28945  hbexwAUX7  29376  nfexwAUX7  29378  nfexdwAUX7  29380  a9eNEW7  29397  ax10NEW7  29400  drex1NEW7  29421  spimeNEW7  29436  cbvexwAUX7  29447  spsbeNEW7  29498  sb8ewAUX7  29521  sbexNEW7  29544  hbexOLD7  29612  nfexOLD7  29615  nfexdOLD7  29618  nfexd2OLD7  29645  cbvexOLD7  29653  cbvexdOLD7  29662  sb8eOLD7  29684