Definition df-mo 2083

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 2134. For another possible definition see mo4 2141. (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 2080	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1540	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2079	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 105	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2091  sb8mo  2093  nfmod  2096  mon  2108  eumo  2111  mobidh  2113  mobid  2114  hbmo1  2117  hbmo  2118  cbvmo  2119  eu5  2127  moabs  2129  exmodc  2130  exmonim  2131  mo2r  2132  mo3h  2133  exmoeudc  2143  2euex  2167  rmo5  2754  moeq  2981  repizf2lem  4251  funeu  5351  dffun8  5354  climmo  11858