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  speimfwOLD  1699  spimfw  1700  ax6ev  1712  cbvexvw  1750  hbe1w  1755  hbe1  1779  excom  1789  axc7e  1802  hbnt  1833  hbex  1884  nfexd  1890  ax6  1959  cbvex  1982  cbvexd  1986  drex1  2029  nfexd2  2034  sbex  2185  eujustALT  2265  spcimegf  3160  spcegf  3162  spcimedv  3165  n0f  3759  eq0  3766  ax6vsep  4534  axnulALT  4536  axpownd  8904  gchi  8928  xfree2  26318  ballotlem2  27327  axextprim  27808  axrepprim  27809  axunprim  27810  axpowprim  27811  axinfprim  27813  axacprim  27814  distel  28073  n0el  29464  pm10.252  30073  hbexgVD  32485  bj-axtd  32963  bj-eximal  32975  bj-nalnaleximiOLD  33010  bj-modalbe  33022  bj-hbext  33045  bj-cbvexv  33078  bj-cbvexdv  33082  bj-drex1v  33107