Definition df-mo 2223

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 2258. For other possible definitions see mo2 2229 and mo4 2269. (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 2219	. 2 wff E* x ph
4	1, 2	wex 1620	. . 3 wff E. x ph
5	1, 2	weu 2218	. . 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  2225  mo2vOLD  2226  mo2vOLDOLD  2227  nfmo1  2231  nfmod2  2233  mobid  2239  exmo  2245  eu5  2246  moabs  2251  exmoeu  2252  sb8mo  2255  cbvmo  2257  2euex  2297  2eu1  2307  bm1.1  2365  rmo5  3001  moeq  3200  funeu  5520  dffun8  5523  modom  7637  climmo  13382  rmoxfrdOLD  27508  rmoxfrd  27509  mont  30027  amosym1  30044  wl-sb8mot  30188  moxfr  30790