Definition df-mo 2259

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 2285. For other possible definitions see mo2 2283 and mo4 2287. (Contributed by NM, 8-Mar-1995.)

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 set x
3	1, 2	wmo 2255	. 2 wff E* x ph
4	1, 2	wex 1547	. . 3 wff E. x ph
5	1, 2	weu 2254	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 177	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  nfmo1  2265  nfmod2  2267  sb8mo  2273  mo2  2283  mobid  2288  cbvmo  2291  exmoeu  2296  moabs  2298  exmo  2299  2euex  2326  rmo5  2884  moeq  3070  funeu  5436  dffun8  5439  modom  7268  climmo  12306  rmoxfrdOLD  23932  rmoxfrd  23933  mont  26063  amosym1  26080  moxfr  26623