Definition df-mo 2209

Description: Define "there exists at most one x such that φ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2235. For other possible definitions see mo2 2233 and mo4 2237. (Contributed by NM, 8-Mar-1995.)

Assertion

Ref	Expression
df-mo	⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		vx	. . 3 setvar x
3	1, 2	wmo 2205	. 2 wff ∃*xφ
4	1, 2	wex 1541	. . 3 wff ∃xφ
5	1, 2	weu 2204	. . 3 wff ∃!xφ
6	4, 5	wi 4	. 2 wff (∃xφ → ∃!xφ)
7	3, 6	wb 176	1 wff (∃*xφ ↔ (∃xφ → ∃!xφ))

This definition is referenced by:  nfmo1  2215  nfmod2  2217  sb8mo  2223  mo2  2233  mobid  2238  cbvmo  2241  exmoeu  2246  moabs  2248  exmo  2249  2euex  2276  rmo5  2828  moeq  3013  dff3  5421