Definition df-mo 2049

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 2099. For another possible definition see mo4 2106. (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 2046	. 2 wff E* x ph
4	1, 2	wex 1506	. . 3 wff E. x ph
5	1, 2	weu 2045	. . 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  2057  sb8mo  2059  nfmod  2062  mon  2074  eumo  2077  mobidh  2079  mobid  2080  hbmo1  2083  hbmo  2084  cbvmo  2085  eu5  2092  moabs  2094  exmodc  2095  exmonim  2096  mo2r  2097  mo3h  2098  exmoeudc  2108  2euex  2132  rmo5  2717  moeq  2939  repizf2lem  4194  funeu  5283  dffun8  5286  climmo  11463