Definition df-mo 2030

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 2080. For another possible definition see mo4 2087. (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 2027	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1492	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2026	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2038  sb8mo  2040  nfmod  2043  mon  2055  eumo  2058  mobidh  2060  mobid  2061  hbmo1  2064  hbmo  2065  cbvmo  2066  eu5  2073  moabs  2075  exmodc  2076  exmonim  2077  mo2r  2078  mo3h  2079  exmoeudc  2089  2euex  2113  rmo5  2692  moeq  2912  repizf2lem  4161  funeu  5241  dffun8  5244  climmo  11305