Definition df-ex 1327

Description: Define existential quantification. E.xph means "there exists at least one set x such that ph is true." Definition of [Margaris] p. 49.

Assertion

Ref	Expression
df-ex	|- (E.xph <-> -. A.x -. ph)

Detailed syntax breakdown of Definition df-ex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	wex 1326	. 2 wff E.xph
4	1	wn 2	. . . 4 wff -. ph
5	4, 2	wal 1296	. . 3 wff A.x -. ph
6	5	wn 2	. 2 wff -. A.x -. ph
7	3, 6	wb 163	1 wff (E.xph <-> -. A.x -. ph)

This definition is referenced by:  a6e 1336  hbex 1353  hbe1 1363  19.8a 1376  alnex 1380  19.9t 1382  exim 1386  19.35 1426  19.30OLD 1437  19.43 1440  19.41OLD 1449  ax9o 1480  a9e 1483  drex1 1517  a4ime 1521  cbvex 1529  equs5e 1567  a4sbe 1613  sb8e 1639  cbvexd 1704  sbex 1739  a12stdy1 1763  a12study 1769  eujustALT 1774  cla4egf 2362  ne0f 2883  eq0 2889  copsexg 3537  axpownd 6105  xfree2 12017  axextprim 13785  axrepprim 13786  axunprim 13787  axpowprim 13788  axinfprim 13790  axacprim 13791  distel 13870  n0el 16248  pm10.252 16307  pm10.56 16317  2exnaln 16326  2nalexn 16340  2exnexn 16341

Copyright terms: Public domain