Definition df-mo 2081

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 2132. For another possible definition see mo4 2139. (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 2078	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1538	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2077	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2089  sb8mo  2091  nfmod  2094  mon  2106  eumo  2109  mobidh  2111  mobid  2112  hbmo1  2115  hbmo  2116  cbvmo  2117  eu5  2125  moabs  2127  exmodc  2128  exmonim  2129  mo2r  2130  mo3h  2131  exmoeudc  2141  2euex  2165  rmo5  2752  moeq  2978  repizf2lem  4244  funeu  5342  dffun8  5345  climmo  11804