Definition df-ex 957

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 956	. 2 wff E.xph
4	1	wn 2	. . . 4 wff -. ph
5	4, 2	wal 950	. . 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 966  hbex 982  hbe1 990  19.8a 1005  alnex 1009  19.9t 1011  19.22 1015  19.35 1051  19.30 1061  19.43 1064  19.41 1071  ax9 1110  a9e 1112  drex1 1139  a4c 1143  cbvex 1149  equs5e 1182  sbea4 1227  sb8e 1246  cbvexd 1303  sbex 1330  a12stdy1 1349  a12study 1355  cla4egf 1836  ne0f 2258  eq0 2265  axpownd 4876

Copyright terms: Public domain