Definition df-mo 2271

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 2306. For other possible definitions see mo2 2277 and mo4 2316. (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 2267	. 2 wff E* x ph
4	1, 2	wex 1659	. . 3 wff E. x ph
5	1, 2	weu 2266	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 187	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  mo2v  2273  mo2vOLD  2274  mo2vOLDOLD  2275  nfmo1  2279  nfmod2  2281  mobid  2287  exmo  2293  eu5  2294  moabs  2299  exmoeu  2300  sb8mo  2303  cbvmo  2305  2euex  2344  2eu1  2354  bm1.1  2412  rmo5  3054  moeq  3253  funeu  5625  dffun8  5628  modom  7779  climmo  13599  rmoxfrdOLD  27963  rmoxfrd  27964  mont  30854  amosym1  30871  wl-sb8mot  31610  moxfr  35242