Definition df-ex 1558

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 1557	. 2
4	1	wn 3	. . . 4
5	4, 2	wal 1556	. . 3
6	5	wn 3	. 2
7	3, 6	wb 178	1

This definition is referenced by:  alnex  1559  2nalexn  1590  2exnaln  1591  19.43OLD  1626  ax5e  1638  speimfw  1665  spimfw  1666  a6ev  1679  cbvexvw  1716  hbe1w  1722  hbe1  1745  excom  1755  a10e  1765  19.8aOLD  1771  hbnt  1798  19.9htOLD  1801  hbex  1858  nfexOLD  1861  nfexd  1868  19.9tOLD  1875  equs5eOLD  1907  ax6  1952  spimeOLD  1958  cbvex  1982  cbvexd  1987  axc9lem5OLD  2013  axc11nOLD  2029  a6eOLD  2031  drex1  2059  nfexd2  2065  spsbeOLD  2149  sbex  2227  eujustALT  2308  spcimegf  3080  spcegf  3082  spcimedv  3085  n0f  3668  eq0  3674  ax6vsep  4427  axnulALT  4429  axpownd  8590  gchi  8613  xfree2  24459  ballotlem2  25512  axextprim  25983  axrepprim  25984  axunprim  25985  axpowprim  25986  axinfprim  25988  axacprim  25989  distel  26261  n0el  27639  pm10.252  28462  pm10.56  28471  hbexgVD  30211  hbexwAUX11  30724  nfexwAUX11  30726  nfexdwAUX11  30728  a6eNEW11  30745  axc11nNEW11  30748  drex1NEW11  30769  spimeNEW11  30784  cbvexwAUX11  30795  spsbeNEW11  30846  sb8ewAUX11  30869  sbexNEW11  30891  hbexOLD11  30959  nfexOLD11  30962  nfexdOLD11  30965  nfexd2OLD11  30992  cbvexOLD11  31000  cbvexdOLD11  31009  sb8eOLD11  31031