Definition df-mo 2059

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 2110. For another possible definition see mo4 2117. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		vx	. . 3 setvar x
3	1, 2	wmo 2056	. 2 wff E* x ph
4	1, 2	wex 1516	. . 3 wff E. x ph
5	1, 2	weu 2055	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 105	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  nfmo1  2067  sb8mo  2069  nfmod  2072  mon  2084  eumo  2087  mobidh  2089  mobid  2090  hbmo1  2093  hbmo  2094  cbvmo  2095  eu5  2103  moabs  2105  exmodc  2106  exmonim  2107  mo2r  2108  mo3h  2109  exmoeudc  2119  2euex  2143  rmo5  2729  moeq  2955  repizf2lem  4221  funeu  5315  dffun8  5318  climmo  11724