Definition df-mo 2274

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 2278 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 2270	. 2 wff E* x ph
4	1, 2	wex 1657	. . 3 wff E. x ph
5	1, 2	weu 2269	. . 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  2276  nfmo1  2280  nfmod2  2282  mobid  2288  exmo  2294  eu5  2295  moabs  2300  exmoeu  2301  sb8mo  2303  cbvmo  2305  2euex  2343  2eu1  2352  bm1.1  2406  rmo5  3046  moeq  3246  funeu  5625  dffun8  5628  modom  7782  climmo  13620  rmoxfrdOLD  28126  rmoxfrd  28127  mont  31074  amosym1  31091  wl-sb8mot  31871  moxfr  35503