Definition df-ex 980

Description: Define existential quantification. ∃xφ means "there exists at least one set x such that φ is true." Definition of [Margaris] p. 49.

Assertion

Ref	Expression
df-ex	⊢ (∃xφ ↔ ¬ ∀x ¬ φ)

Detailed syntax breakdown of Definition df-ex

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3	1, 2	wex 979	. 2 wff ∃xφ
4	1	wn 2	. . . 4 wff ¬ φ
5	4, 2	wal 953	. . 3 wff ∀x ¬ φ
6	5	wn 2	. 2 wff ¬ ∀x ¬ φ
7	3, 6	wb 146	1 wff (∃xφ ↔ ¬ ∀x ¬ φ)

This definition is referenced by:  a6e 989  hbex 1005  hbe1 1015  19.8a 1028  alnex 1032  19.9t 1034  19.22 1038  19.35 1074  19.30 1084  19.43 1087  19.41 1094  ax9o 1121  a9e 1124  drex1 1155  a4ime 1159  cbvex 1165  equs5e 1197  a4sbe 1242  sb8e 1261  cbvexd 1320  sbex 1347  a12stdy1 1371  a12study 1377  cla4egf 1858  ne0f 2284  eq0 2291  axpownd 4936

Copyright terms: Public domain