Definition df-mo 2275

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 2315. For other possible definitions see mo2 2282 and mo4 2334. (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 2271	. 2 wff E* x ph
4	1, 2	wex 1591	. . 3 wff E. x ph
5	1, 2	weu 2270	. . 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  2277  mo2vOLD  2278  mo2vOLDOLD  2279  nfmo1  2284  nfmod2  2286  mobid  2292  exmo  2299  eu5  2300  moabs  2305  exmoeu  2306  exmoeuOLD  2307  sb8mo  2312  cbvmo  2314  mo2OLD  2331  2euex  2370  2eu1  2381  bm1.1  2445  rmo5  3075  moeq  3274  funeu  5605  dffun8  5608  modom  7712  climmo  13331  rmoxfrdOLD  27055  rmoxfrd  27056  mont  29439  amosym1  29456  wl-sb8mot  29588  moxfr  30217