Definition df-ex 1548

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 1547	. 2 wff E. x ph
4	1	wn 3	. . . 4 wff -. ph
5	4, 2	wal 1546	. . 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  1549  2nalexn  1579  19.43OLD  1613  ax17e  1625  speimfw  1652  spimfw  1653  a9ev  1664  19.8wOLD  1701  19.9vOLD  1706  cbvexvw  1713  hbe1w  1719  hbe1  1742  excom  1752  a6e  1763  19.8aOLD  1768  hbnt  1795  19.9htOLD  1799  spimehOLD  1836  hbex  1859  nfexOLD  1862  nfexd  1869  19.9tOLD  1876  equs5eOLD  1907  ax9  1949  spimeOLD  1957  ax12olem5OLD  1981  ax10OLD  1998  a9eOLD  2000  drex1  2034  nfexd2  2040  cbvex  2060  cbvexd  2064  spsbe  2132  sbex  2186  eujustALT  2265  spcimegf  2998  spcegf  3000  spcimedv  3003  n0f  3604  eq0  3610  ax9vsep  4302  axnulALT  4304  axpownd  8440  gchi  8463  xfree2  23909  ballotlem2  24707  axextprim  25111  axrepprim  25112  axunprim  25113  axpowprim  25114  axinfprim  25116  axacprim  25117  distel  25382  n0el  26606  pm10.252  27432  pm10.56  27441  2exnaln  27448  hbexgVD  28736  hbexwAUX7  29167  nfexwAUX7  29169  nfexdwAUX7  29171  a9eNEW7  29188  ax10NEW7  29191  drex1NEW7  29212  spimeNEW7  29227  cbvexwAUX7  29236  spsbeNEW7  29287  sb8ewAUX7  29307  sbexNEW7  29330  hbexOLD7  29381  nfexOLD7  29384  nfexdOLD7  29387  nfexd2OLD7  29414  cbvexOLD7  29422  cbvexdOLD7  29431  sb8eOLD7  29453