Definition df-mo 2040

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 2090. For another possible definition see mo4 2097. (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 2037	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1502	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2036	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2048  sb8mo  2050  nfmod  2053  mon  2065  eumo  2068  mobidh  2070  mobid  2071  hbmo1  2074  hbmo  2075  cbvmo  2076  eu5  2083  moabs  2085  exmodc  2086  exmonim  2087  mo2r  2088  mo3h  2089  exmoeudc  2099  2euex  2123  rmo5  2703  moeq  2924  repizf2lem  4173  funeu  5253  dffun8  5256  climmo  11319