Definition df-mo 2028

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

This definition is referenced by:  nfmo1  2036  sb8mo  2038  nfmod  2041  mon  2053  eumo  2056  mobidh  2058  mobid  2059  hbmo1  2062  hbmo  2063  cbvmo  2064  eu5  2071  moabs  2073  exmodc  2074  exmonim  2075  mo2r  2076  mo3h  2077  exmoeudc  2087  2euex  2111  rmo5  2690  moeq  2910  repizf2lem  4156  funeu  5233  dffun8  5236  climmo  11274