Definition df-mo 2018

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 2068. For another possible definition see mo4 2075. (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 2015	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1480	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2014	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 104	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2026  sb8mo  2028  nfmod  2031  mon  2043  eumo  2046  mobidh  2048  mobid  2049  hbmo1  2052  hbmo  2053  cbvmo  2054  eu5  2061  moabs  2063  exmodc  2064  exmonim  2065  mo2r  2066  mo3h  2067  exmoeudc  2077  2euex  2101  rmo5  2681  moeq  2901  repizf2lem  4140  funeu  5213  dffun8  5216  climmo  11239