Definition df-mo 2059

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 2109. For another possible definition see mo4 2116. (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 2056	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1516	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2055	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2067  sb8mo  2069  nfmod  2072  mon  2084  eumo  2087  mobidh  2089  mobid  2090  hbmo1  2093  hbmo  2094  cbvmo  2095  eu5  2102  moabs  2104  exmodc  2105  exmonim  2106  mo2r  2107  mo3h  2108  exmoeudc  2118  2euex  2142  rmo5  2727  moeq  2952  repizf2lem  4216  funeu  5310  dffun8  5313  climmo  11694