Definition df-ex 1017

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

This definition is referenced by:  a6e 1026  hbex 1042  hbe1 1052  19.8a 1065  alnex 1069  19.9t 1071  19.22 1075  19.35 1111  19.30 1121  19.43 1124  19.41 1131  ax9o 1158  a9e 1161  drex1 1193  a4ime 1197  cbvex 1203  equs5e 1235  a4sbe 1280  sb8e 1300  cbvexd 1359  sbex 1387  a12stdy1 1411  a12study 1417  cla4egf 1907  ne0f 2340  eq0 2347  axpownd 5107  xfree2 10654

Copyright terms: Public domain