Definition df-mo 1949

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 1999. For another possible definition see mo4 2006. (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 1946	. 2 wff E* x ph
4	1, 2	wex 1424	. . 3 wff E. x ph
5	1, 2	weu 1945	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 103	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  nfmo1  1957  sb8mo  1959  nfmod  1962  mon  1974  eumo  1977  mobidh  1979  mobid  1980  hbmo1  1983  hbmo  1984  cbvmo  1985  eu5  1992  moabs  1994  exmodc  1995  exmonim  1996  mo2r  1997  mo3h  1998  exmoeudc  2008  2euex  2032  rmo5  2578  moeq  2781  repizf2lem  3973  funeu  5007  dffun8  5010  climmo  10584