Definition df-ex 983

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 982	. 2 wff E.xph
4	1	wn 2	. . . 4 wff -. ph
5	4, 2	wal 956	. . 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 992  hbex 1008  hbe1 1018  19.8a 1031  alnex 1035  19.9t 1037  19.22 1041  19.35 1077  19.30 1087  19.43 1090  19.41 1097  ax9o 1124  a9e 1127  drex1 1158  a4ime 1162  cbvex 1168  equs5e 1200  a4sbe 1245  sb8e 1264  cbvexd 1323  sbex 1350  a12stdy1 1374  a12study 1380  cla4egf 1864  ne0f 2291  eq0 2298  axpownd 4965

Copyright terms: Public domain