Definition df-mo 2058

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 2108. For another possible definition see mo4 2115. (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 2055	. 2 wff E* x ph
4	1, 2	wex 1515	. . 3 wff E. x ph
5	1, 2	weu 2054	. . 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  2066  sb8mo  2068  nfmod  2071  mon  2083  eumo  2086  mobidh  2088  mobid  2089  hbmo1  2092  hbmo  2093  cbvmo  2094  eu5  2101  moabs  2103  exmodc  2104  exmonim  2105  mo2r  2106  mo3h  2107  exmoeudc  2117  2euex  2141  rmo5  2726  moeq  2948  repizf2lem  4205  funeu  5296  dffun8  5299  climmo  11609