Definition df-mo 2071

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

Assertion

Ref	Expression
df-mo	|- (E*xph <-> (E.xph -> E!xph))

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 set x
3	1, 2	wmo 2067	. 2 wff E*xph
4	1, 2	wex 1644	. . 3 wff E.xph
5	1, 2	weu 2066	. . 3 wff E!xph
6	4, 5	wi 3	. 2 wff (E.xph -> E!xph)
7	3, 6	wb 231	1 wff (E*xph <-> (E.xph -> E!xph))

This definition is referenced by:  mo2 2089  mobid 2094  hbmo1 2096  hbmo 2097  cbvmo 2098  exmoeu 2103  moabs 2105  exmo 2106  2euex 2133  moeq 2707  funeu 4586  dffun8 4589  mont 15106  amosym1 15197

Copyright terms: Public domain