Definition df-ex 1588

Description: Define existential quantification. means "there exists at least one set such that is true." Definition of [Margaris] p. 49. (Contributed by NM, 10-Jan-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 1587	. 2
4	1	wn 3	. . . 4
5	4, 2	wal 1368	. . 3
6	5	wn 3	. 2
7	3, 6	wb 184	1

This definition is referenced by:  alnex  1589  2nalexn  1620  2exnaln  1621  19.43OLD  1662  ax5e  1673  speimfw  1698  spimfw  1699  ax6ev  1711  cbvexvw  1749  hbe1w  1754  hbe1  1778  excom  1788  axc7e  1798  hbnt  1829  hbex  1873  nfexd  1879  ax6  1948  cbvex  1971  cbvexd  1975  drex1  2025  nfexd2  2030  sbex  2182  eujustALT  2262  spcimegf  3131  spcegf  3133  spcimedv  3136  n0f  3727  eq0  3734  ax6vsep  4499  axnulALT  4501  axpownd  8852  gchi  8876  xfree2  25968  ballotlem2  26989  axextprim  27470  axrepprim  27471  axunprim  27472  axpowprim  27473  axinfprim  27475  axacprim  27476  distel  27735  n0el  29126  pm10.252  29735  hbexgVD  31923  bj-axtd  32410  bj-eximal  32411  bj-nalnaleximiOLD  32446  bj-modalbe  32458  bj-hbext  32481  bj-cbvexv  32514  bj-cbvexdv  32518  bj-drex1v  32543