Definition df-mo 1947

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 1997. For another possible definition see mo4 2004. (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 1944	. 2 wff E* x ph
4	1, 2	wex 1422	. . 3 wff E. x ph
5	1, 2	weu 1943	. . 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  1955  sb8mo  1957  nfmod  1960  mon  1972  eumo  1975  mobidh  1977  mobid  1978  hbmo1  1981  hbmo  1982  cbvmo  1983  eu5  1990  moabs  1992  exmodc  1993  exmonim  1994  mo2r  1995  mo3h  1996  exmoeudc  2006  2euex  2030  rmo5  2575  moeq  2778  repizf2lem  3961  funeu  4991  dffun8  4994  climmo  10509