Definition df-mo 2462

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 2494. For other possible definitions see mo2 2466 and mo4 2504. (Contributed by NM, 8-Mar-1995.)

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 2458	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1694	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2457	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 194	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  mo2v  2464  nfmo1  2468  nfmod2  2470  mobid  2476  exmo  2482  eu5  2483  moabs  2488  exmoeu  2489  sb8mo  2491  cbvmo  2493  2euex  2531  2eu1  2540  bm1.1  2594  rmo5  3138  moeq  3348  funeu  5813  dffun8  5816  modom  8023  climmo  14084  rmoxfrdOLD  28509  rmoxfrd  28510  mont  31371  amosym1  31388  wl-sb8mot  32322  moxfr  36056