Definition df-mo 2273

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 2309. For other possible definitions see mo2 2279 and mo4 2323. (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 setvar x
3	1, 2	wmo 2269	. 2 wff E* x ph
4	1, 2	wex 1599	. . 3 wff E. x ph
5	1, 2	weu 2268	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 184	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  mo2v  2275  mo2vOLD  2276  mo2vOLDOLD  2277  nfmo1  2281  nfmod2  2283  mobid  2289  exmo  2295  eu5  2296  moabs  2301  exmoeu  2302  sb8mo  2306  cbvmo  2308  mo2OLD  2320  2euex  2352  2eu1  2362  bm1.1  2426  rmo5  3062  moeq  3261  funeu  5602  dffun8  5605  modom  7722  climmo  13362  rmoxfrdOLD  27369  rmoxfrd  27370  mont  29850  amosym1  29867  wl-sb8mot  29999  moxfr  30600