Definition df-ex 1552

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

This definition is referenced by:  alnex  1553  2nalexn  1583  19.43OLD  1617  ax17e  1629  speimfw  1656  spimfw  1657  a9ev  1669  19.8wOLD  1706  19.9vOLD  1711  cbvexvw  1718  hbe1w  1724  hbe1  1747  excom  1757  a6e  1768  19.8aOLD  1773  hbnt  1800  19.9htOLD  1804  spimehOLD  1841  hbex  1864  nfexOLD  1867  nfexd  1874  19.9tOLD  1881  equs5eOLD  1912  ax9  1954  spimeOLD  1960  cbvex  1984  cbvexd  1989  ax12olem5OLD  2016  ax10OLD  2033  a9eOLD  2035  drex1  2060  nfexd2  2066  spsbeOLD  2149  sbex  2207  eujustALT  2286  spcimegf  3032  spcegf  3034  spcimedv  3037  n0f  3638  eq0  3644  ax9vsep  4337  axnulALT  4339  axpownd  8481  gchi  8504  xfree2  23953  ballotlem2  24751  axextprim  25155  axrepprim  25156  axunprim  25157  axpowprim  25158  axinfprim  25160  axacprim  25161  distel  25436  n0el  26721  pm10.252  27546  pm10.56  27555  2exnaln  27562  hbexgVD  29091  hbexwAUX7  29522  nfexwAUX7  29524  nfexdwAUX7  29526  a9eNEW7  29543  ax10NEW7  29546  drex1NEW7  29567  spimeNEW7  29582  cbvexwAUX7  29593  spsbeNEW7  29644  sb8ewAUX7  29667  sbexNEW7  29690  hbexOLD7  29758  nfexOLD7  29761  nfexdOLD7  29764  nfexd2OLD7  29791  cbvexOLD7  29799  cbvexdOLD7  29808  sb8eOLD7  29830