Definition df-mo 1376

Description: Define "there exists at most one x such that φ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 1394. For other possible definitions see mo2 1393 and mo4 1396.

Assertion

Ref	Expression
df-mo	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 set x
3	1, 2	wmo 1374	. 2 wff ∃*xφ
4	1, 2	wex 977	. . 3 wff ∃xφ
5	1, 2	weu 1373	. . 3 wff ∃!xφ
6	4, 5	wi 3	. 2 wff (∃xφ → ∃!xφ)
7	3, 6	wb 146	1 wff (∃*xφ ↔ (∃xφ → ∃!xφ))

This definition is referenced by:  mo2 1393  mobid 1397  hbmo1 1399  hbmo 1400  cbvmo 1401  exmoeu 1406  moabs 1408  exmo 1409  moeq 1911

Copyright terms: Public domain