Definition df-ex 1645

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 1644	. 2 wff E.xph
4	1	wn 2	. . . 4 wff -. ph
5	4, 2	wal 1613	. . 3 wff A.x -. ph
6	5	wn 2	. 2 wff -. A.x -. ph
7	3, 6	wb 231	1 wff (E.xph <-> -. A.x -. ph)

This definition is referenced by:  a6e 1654  hbex 1671  hbe1 1681  19.8a 1694  alnex 1698  19.9t 1700  exim 1704  19.35 1741  19.43 1754  ax9o 1791  a9e 1794  drex1 1826  a4ime 1831  cbvex 1838  equs5e 1871  a4sbe 1918  sb8e 1938  cbvexd 2000  sbex 2032  a12stdy1 2056  a12study 2062  eujustALT 2069  cla4egf 2634  n0f 3122  eq0 3128  copsexg 3732  sucdom2 5854  axpownd 6548  xfree2 13006  axextprim 14667  axrepprim 14668  axunprim 14669  axpowprim 14670  axinfprim 14672  axacprim 14673  distel 14758  elsingles 15022  n0el 17333  pm10.252 17392  pm10.56 17402  2exnaln 17411  2nalexn 17425  2exnexn 17426

Copyright terms: Public domain