Definition df-mo 2023

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 2073. For another possible definition see mo4 2080. (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 2020	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1485	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2019	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 104	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2031  sb8mo  2033  nfmod  2036  mon  2048  eumo  2051  mobidh  2053  mobid  2054  hbmo1  2057  hbmo  2058  cbvmo  2059  eu5  2066  moabs  2068  exmodc  2069  exmonim  2070  mo2r  2071  mo3h  2072  exmoeudc  2082  2euex  2106  rmo5  2685  moeq  2905  repizf2lem  4147  funeu  5223  dffun8  5226  climmo  11261