Definition df-mo 1901

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

Assertion

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

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 1898	. 2 wff E*xph
4	1, 2	wex 1378	. . 3 wff E.xph
5	1, 2	weu 1897	. . 3 wff E!xph
6	4, 5	wi 4	. 2 wff (E.xph -> E!xph)
7	3, 6	wb 98	1 wff (E*xph <-> (E.xph -> E!xph))

This definition is referenced by:  nfmo1  1909  sb8mo  1911  nfmod  1914  mon  1926  eumo  1929  mobidh  1931  mobid  1932  hbmo1  1935  hbmo  1936  cbvmo  1937  eu5  1944  moabs  1946  exmodc  1947  exmonim  1948  mo2r  1949  mo3h  1950  exmoeudc  1960  2euex  1984  rmo5  2519  moeq  2710  repizf2lem  3905  funeu  4869  dffun8  4872