Definition df-mo 2463

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 2495. For other possible definitions see mo2 2467 and mo4 2505. (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 2459	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1695	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2458	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 195	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  mo2v  2465  nfmo1  2469  nfmod2  2471  mobid  2477  exmo  2483  eu5  2484  moabs  2489  exmoeu  2490  sb8mo  2492  cbvmo  2494  2euex  2532  2eu1  2541  bm1.1  2595  rmo5  3139  moeq  3349  funeu  5828  dffun8  5831  modom  8046  climmo  14136  rmoxfrdOLD  28716  rmoxfrd  28717  mont  31578  amosym1  31595  wl-sb8mot  32539  moxfr  36273