Definition df-mo 1945

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 1995. For another possible definition see mo4 2002. (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 1942	. 2 wff E* x ph
4	1, 2	wex 1421	. . 3 wff E. x ph
5	1, 2	weu 1941	. . 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  1953  sb8mo  1955  nfmod  1958  mon  1970  eumo  1973  mobidh  1975  mobid  1976  hbmo1  1979  hbmo  1980  cbvmo  1981  eu5  1988  moabs  1990  exmodc  1991  exmonim  1992  mo2r  1993  mo3h  1994  exmoeudc  2004  2euex  2028  rmo5  2569  moeq  2767  repizf2lem  3935  funeu  4946  dffun8  4949  climmo  10137