Definition df-ex 1613

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 1612	. 2
4	1	wn 3	. . . 4
5	4, 2	wal 1393	. . 3
6	5	wn 3	. 2
7	3, 6	wb 184	1

This definition is referenced by:  alnex  1614  eximal  1615  2nalexn  1649  2exnaln  1650  19.43OLD  1694  speimfw  1735  speimfwOLD  1736  spimfw  1737  ax6ev  1749  cbvexvw  1810  hbe1w  1815  hbe1  1839  excom  1849  axc7e  1862  hbnt  1894  hbex  1946  nfexd  1952  ax6  2003  cbvex  2022  cbvexd  2026  drex1  2069  nfexd2  2074  sbex  2207  eujustALT  2285  spcimegf  3188  spcegf  3190  spcimedv  3193  n0f  3793  eq0  3800  ax6vsep  4577  axnulALT  4579  axpownd  8999  gchi  9023  ballotlem2  28427  axextprim  29073  axrepprim  29074  axunprim  29075  axpowprim  29076  axinfprim  29078  axacprim  29079  distel  29236  n0el  30600  pm10.252  31266  hbexgVD  33706  bj-axtd  34182  bj-nalnaleximiOLD  34222  bj-modalbe  34241  bj-hbext  34264  bj-cbvexv  34297  bj-cbvexdv  34301  bj-drex1v  34327