Definition df-mo 2604

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 2637. For other possible definitions see mo2 2608 and mo4 2647. (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 2600	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1845	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2599	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 196	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  mo2v  2606  nfmo1  2610  nfmod2  2612  mobid  2618  exmo  2624  eu5  2625  eumo  2628  moabs  2631  exmoeu  2632  sb8mo  2634  cbvmo  2636  2euex  2674  2eu1  2683  bm1.1  2737  rmo5  3293  moeq  3515  funeu  6066  dffun8  6069  modom  8318  climmo  14479  rmoxfrdOLD  29632  rmoxfrd  29633  mont  32706  amosym1  32723  wl-sb8mot  33665  nexmo  34328  moxfr  37749