Definition df-mo 2017

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 2067. For another possible definition see mo4 2074. (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 2014	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1479	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2013	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 104	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  2025  sb8mo  2027  nfmod  2030  mon  2042  eumo  2045  mobidh  2047  mobid  2048  hbmo1  2051  hbmo  2052  cbvmo  2053  eu5  2060  moabs  2062  exmodc  2063  exmonim  2064  mo2r  2065  mo3h  2066  exmoeudc  2076  2euex  2100  rmo5  2679  moeq  2896  repizf2lem  4134  funeu  5207  dffun8  5210  climmo  11225