Definition df-ex 1582

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

This definition is referenced by:  alnex  1583  2nalexn  1614  2exnaln  1615  19.43OLD  1651  ax5e  1663  speimfw  1690  spimfw  1691  ax6ev  1703  cbvexvw  1741  hbe1w  1746  hbe1  1770  excom  1780  ax10e  1790  hbnt  1820  hbex  1862  nfexd  1868  ax6  1938  cbvex  1961  cbvexd  1965  drex1  2010  nfexd2  2015  sbex  2167  eujustALT  2247  spcimegf  3029  spcegf  3031  spcimedv  3034  n0f  3622  eq0  3629  ax6vsep  4392  axnulALT  4394  axpownd  8714  gchi  8737  xfree2  25528  ballotlem2  26574  axextprim  27054  axrepprim  27055  axunprim  27056  axpowprim  27057  axinfprim  27059  axacprim  27060  distel  27319  n0el  28676  pm10.252  29286  pm10.56  29295  hbexgVD  31220  bj-axtd  31666  bj-eximal  31667  bj-speimfw  31700  bj-cbvexv  31739  bj-cbvexdv  31743  bj-drex1v  31768