Definition df-mo 2315

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 2347. For other possible definitions see mo2 2319 and mo4 2357. (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 2311	. 2 wff E* x ph
4	1, 2	wex 1674	. . 3 wff E. x ph
5	1, 2	weu 2310	. . 3 wff E! x ph
6	4, 5	wi 4	. 2 wff ( E. x ph -> E! x ph )
7	3, 6	wb 189	1 wff ( E* x ph <-> ( E. x ph -> E! x ph ) )

This definition is referenced by:  mo2v  2317  nfmo1  2321  nfmod2  2323  mobid  2329  exmo  2335  eu5  2336  moabs  2341  exmoeu  2342  sb8mo  2344  cbvmo  2346  2euex  2384  2eu1  2393  bm1.1  2447  rmo5  3023  moeq  3226  funeu  5629  dffun8  5632  modom  7804  climmo  13676  rmoxfrdOLD  28184  rmoxfrd  28185  mont  31119  amosym1  31136  wl-sb8mot  31953  moxfr  35580