Definition df-mo 2086

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 2137. For another possible definition see mo4 2144. (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 2083	. 2 wff E* x ph
4	1, 2	wex 1541	. . 3 wff E. x ph
5	1, 2	weu 2082	. . 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  2094  sb8mo  2096  nfmod  2099  mon  2111  eumo  2114  mobidh  2116  mobid  2117  hbmo1  2120  hbmo  2121  cbvmo  2122  eu5  2130  moabs  2132  exmodc  2133  exmonim  2134  mo2r  2135  mo3h  2136  exmoeudc  2146  2euex  2170  rmo5  2767  moeq  2994  repizf2lem  4276  funeu  5379  dffun8  5382  climmo  11987