Definition df-mo 2090

Description: Define "there exists at most one 𝑥 such that 𝜑". Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2141. For another possible definition see mo4 2148. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-mo	⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3	1, 2	wmo 2087	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1545	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2086	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2098  sb8mo  2100  nfmod  2103  mon  2115  eumo  2118  mobidh  2120  mobid  2121  hbmo1  2124  hbmo  2125  cbvmo  2126  eu5  2134  moabs  2136  exmodc  2137  exmonim  2138  mo2r  2139  mo3h  2140  exmoeudc  2150  2euex  2174  rmo5  2773  moeq  3001  repizf2lem  4296  funeu  5400  dffun8  5403  climmo  12045