Definition df-mo 2003

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 2053. For another possible definition see mo4 2060. (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 2000	. 2 wff E* x ph
4	1, 2	wex 1468	. . 3 wff E. x ph
5	1, 2	weu 1999	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 104	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  nfmo1  2011  sb8mo  2013  nfmod  2016  mon  2028  eumo  2031  mobidh  2033  mobid  2034  hbmo1  2037  hbmo  2038  cbvmo  2039  eu5  2046  moabs  2048  exmodc  2049  exmonim  2050  mo2r  2051  mo3h  2052  exmoeudc  2062  2euex  2086  rmo5  2646  moeq  2859  repizf2lem  4085  funeu  5148  dffun8  5151  climmo  11067