Definition df-mo 2057

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 2107. For another possible definition see mo4 2114. (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 2054	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1514	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2053	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2065  sb8mo  2067  nfmod  2070  mon  2082  eumo  2085  mobidh  2087  mobid  2088  hbmo1  2091  hbmo  2092  cbvmo  2093  eu5  2100  moabs  2102  exmodc  2103  exmonim  2104  mo2r  2105  mo3h  2106  exmoeudc  2116  2euex  2140  rmo5  2725  moeq  2947  repizf2lem  4204  funeu  5295  dffun8  5298  climmo  11551