Definition df-mo 1977

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 2027. For another possible definition see mo4 2034. (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 1974	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1449	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 1973	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 104	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  nfmo1  1985  sb8mo  1987  nfmod  1990  mon  2002  eumo  2005  mobidh  2007  mobid  2008  hbmo1  2011  hbmo  2012  cbvmo  2013  eu5  2020  moabs  2022  exmodc  2023  exmonim  2024  mo2r  2025  mo3h  2026  exmoeudc  2036  2euex  2060  rmo5  2618  moeq  2826  repizf2lem  4043  funeu  5104  dffun8  5107  climmo  10953