Definition df-mo 2004

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 2054. For another possible definition see mo4 2061. (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 2001	. 2 wff E* x ph
4	1, 2	wex 1469	. . 3 wff E. x ph
5	1, 2	weu 2000	. . 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  2012  sb8mo  2014  nfmod  2017  mon  2029  eumo  2032  mobidh  2034  mobid  2035  hbmo1  2038  hbmo  2039  cbvmo  2040  eu5  2047  moabs  2049  exmodc  2050  exmonim  2051  mo2r  2052  mo3h  2053  exmoeudc  2063  2euex  2087  rmo5  2649  moeq  2863  repizf2lem  4093  funeu  5156  dffun8  5159  climmo  11099