Definition df-ex 679

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

This definition is referenced by:  a6e 688  hbex 701  hbe1 709  19.8a 712  alnex 716  19.9r 718  19.9t 719  19.22 722  19.35 754  19.30 764  19.43 767  19.41 774  ax9 807  a9e 809  del40 839  del41 840  del42 841  a4c 843  cbvex 849  sbea4 894  sb8e 919  cbvexd 978  sbex 998  cla4egf 1395  cla4ev 1401  n0f 1713  eq0 1719  axpownd 3747

metamath.org