Definition df-mo 1904

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 1954. For another possible definition see mo4 1961. (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 1901	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1381	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 1900	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 98	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  1912  sb8mo  1914  nfmod  1917  mon  1929  eumo  1932  mobidh  1934  mobid  1935  hbmo1  1938  hbmo  1939  cbvmo  1940  eu5  1947  moabs  1949  exmodc  1950  exmonim  1951  mo2r  1952  mo3h  1953  exmoeudc  1963  2euex  1987  rmo5  2525  moeq  2716  repizf2lem  3914  funeu  4926  dffun8  4929  climmo  9819