Definition df-mo 2046

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 2096. For another possible definition see mo4 2103. (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 2043	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1503	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2042	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2054  sb8mo  2056  nfmod  2059  mon  2071  eumo  2074  mobidh  2076  mobid  2077  hbmo1  2080  hbmo  2081  cbvmo  2082  eu5  2089  moabs  2091  exmodc  2092  exmonim  2093  mo2r  2094  mo3h  2095  exmoeudc  2105  2euex  2129  rmo5  2714  moeq  2935  repizf2lem  4190  funeu  5279  dffun8  5282  climmo  11441