Definition df-ex 979

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

This definition is referenced by:  a6e 988  hbex 1004  hbe1 1014  19.8a 1027  alnex 1031  19.9t 1033  19.22 1037  19.35 1073  19.30 1083  19.43 1086  19.41 1093  ax9o 1120  a9e 1123  drex1 1154  a4ime 1158  cbvex 1164  equs5e 1196  a4sbe 1241  sb8e 1260  cbvexd 1319  sbex 1346  a12stdy1 1370  a12study 1376  cla4egf 1857  ne0f 2283  eq0 2290  axpownd 4933

Copyright terms: Public domain