Definition df-mo 2018

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 2068. For another possible definition see mo4 2075. (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 2015	. 2 wff E* x ph
4	1, 2	wex 1480	. . 3 wff E. x ph
5	1, 2	weu 2014	. . 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  2026  sb8mo  2028  nfmod  2031  mon  2043  eumo  2046  mobidh  2048  mobid  2049  hbmo1  2052  hbmo  2053  cbvmo  2054  eu5  2061  moabs  2063  exmodc  2064  exmonim  2065  mo2r  2066  mo3h  2067  exmoeudc  2077  2euex  2101  rmo5  2680  moeq  2900  repizf2lem  4139  funeu  5212  dffun8  5215  climmo  11235