Definition df-ex 1566

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

This definition is referenced by:  alnex  1567  2nalexn  1598  2exnaln  1599  19.43OLD  1634  ax5e  1646  speimfw  1673  spimfw  1674  a6ev  1687  cbvexvw  1724  hbe1w  1730  hbe1  1753  excom  1763  a10e  1773  19.8aOLD  1779  hbnt  1806  19.9htOLD  1809  hbex  1866  nfexOLD  1869  nfexd  1876  19.9tOLD  1883  equs5eOLD  1915  ax6  1960  spimeOLD  1966  cbvex  1990  cbvexd  1995  axc9lem5OLD  2021  axc11nOLD  2037  a6eOLD  2039  drex1  2067  nfexd2  2073  spsbeOLD  2157  sbex  2235  eujustALT  2316  spcimegf  3091  spcegf  3093  spcimedv  3096  n0f  3681  eq0  3687  ax6vsep  4443  axnulALT  4445  axpownd  8647  gchi  8670  xfree2  24971  ballotlem2  26021  axextprim  26492  axrepprim  26493  axunprim  26494  axpowprim  26495  axinfprim  26497  axacprim  26498  distel  26770  n0el  28148  pm10.252  28787  pm10.56  28796  hbexgVD  30488  hbexwAUX11  31001  nfexwAUX11  31003  nfexdwAUX11  31005  a6eNEW11  31022  axc11nNEW11  31025  drex1NEW11  31046  spimeNEW11  31061  cbvexwAUX11  31072  spsbeNEW11  31123  sb8ewAUX11  31146  sbexNEW11  31168  hbexOLD11  31236  nfexOLD11  31239  nfexdOLD11  31242  nfexd2OLD11  31269  cbvexOLD11  31277  cbvexdOLD11  31286  sb8eOLD11  31308