Definition df-ex 978

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 977	. 2 wff ∃xφ
4	1	wn 2	. . . 4 wff ¬ φ
5	4, 2	wal 951	. . 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 987  hbex 1003  hbe1 1012  19.8a 1025  alnex 1029  19.9t 1031  19.22 1035  19.35 1071  19.30 1081  19.43 1084  19.41 1091  ax9o 1118  a9e 1121  drex1 1152  a4ime 1156  cbvex 1162  equs5e 1194  a4sbe 1238  sb8e 1257  cbvexd 1316  sbex 1343  a12stdy1 1365  a12study 1371  cla4egf 1852  ne0f 2277  eq0 2284  axpownd 4925

Copyright terms: Public domain