Definition df-mo 1614

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 1634. For other possible definitions see mo2 1633 and mo4 1636.

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 1610	. 2 wff E*xph
4	1, 2	wex 1164	. . 3 wff E.xph
5	1, 2	weu 1609	. . 3 wff E!xph
6	4, 5	wi 3	. 2 wff (E.xph -> E!xph)
7	3, 6	wb 162	1 wff (E*xph <-> (E.xph -> E!xph))

This definition is referenced by:  mo2 1633  mobid 1637  hbmo1 1639  hbmo 1640  cbvmo 1641  exmoeu 1646  moabs 1648  exmo 1649  2euex 1681  moeq 2264  funeu 4255  dffun8 4259  mont 13889  amosym1 13980

Copyright terms: Public domain