Definition df-ex 1552

Description: Define existential quantification. means "there exists at least one set such that is true." Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-ex

Detailed syntax breakdown of Definition df-ex

Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3	1, 2	wex 1551	. 2
4	1	wn 3	. . . 4
5	4, 2	wal 1550	. . 3
6	5	wn 3	. 2
7	3, 6	wb 178	1

This definition is referenced by:  alnex  1553  2nalexn  1583  19.43OLD  1618  ax17e  1630  speimfw  1657  spimfw  1658  a9ev  1671  19.8wOLD  1708  19.9vOLD  1713  cbvexvw  1720  hbe1w  1726  hbe1  1749  excom  1759  a6e  1770  19.8aOLD  1775  hbnt  1802  19.9htOLD  1806  spimehOLD  1843  hbex  1866  nfexOLD  1869  nfexd  1876  19.9tOLD  1883  equs5eOLD  1915  ax9  1957  spimeOLD  1963  cbvex  1987  cbvexd  1992  ax12olem5OLD  2019  ax10OLD  2036  a9eOLD  2038  drex1  2063  nfexd2  2069  spsbeOLD  2153  sbex  2212  eujustALT  2291  spcimegf  3039  spcegf  3041  spcimedv  3044  n0f  3624  eq0  3630  ax9vsep  4368  axnulALT  4370  axpownd  8527  gchi  8550  xfree2  23999  ballotlem2  24850  axextprim  25254  axrepprim  25255  axunprim  25256  axpowprim  25257  axinfprim  25259  axacprim  25260  distel  25535  n0el  26889  pm10.252  27712  pm10.56  27721  2exnaln  27728  hbexgVD  29259  hbexwAUX7  29690  nfexwAUX7  29692  nfexdwAUX7  29694  a9eNEW7  29711  ax10NEW7  29714  drex1NEW7  29735  spimeNEW7  29750  cbvexwAUX7  29761  spsbeNEW7  29812  sb8ewAUX7  29835  sbexNEW7  29858  hbexOLD7  29926  nfexOLD7  29929  nfexdOLD7  29932  nfexd2OLD7  29959  cbvexOLD7  29967  cbvexdOLD7  29976  sb8eOLD7  29998