Definition df-ex 981

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 980	. 2 wff E.xph
4	1	wn 2	. . . 4 wff -. ph
5	4, 2	wal 954	. . 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 990  hbex 1006  hbe1 1016  19.8a 1029  alnex 1033  19.9t 1035  19.22 1039  19.35 1075  19.30 1085  19.43 1088  19.41 1095  ax9o 1122  a9e 1125  drex1 1156  a4ime 1160  cbvex 1166  equs5e 1198  a4sbe 1243  sb8e 1262  cbvexd 1321  sbex 1348  a12stdy1 1372  a12study 1378  cla4egf 1861  ne0f 2287  eq0 2294  axpownd 4953

Copyright terms: Public domain