Definition df-mo 2503

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 2536. For other possible definitions see mo2 2507 and mo4 2546. (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 2499	. 2 wff ∃*𝑥𝜑
4	1, 2	wex 1744	. . 3 wff ∃𝑥𝜑
5	1, 2	weu 2498	. . 3 wff ∃!𝑥𝜑
6	4, 5	wi 4	. 2 wff (∃𝑥𝜑 → ∃!𝑥𝜑)
7	3, 6	wb 196	1 wff (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))

This definition is referenced by:  mo2v  2505  nfmo1  2509  nfmod2  2511  mobid  2517  exmo  2523  eu5  2524  eumo  2527  moabs  2530  exmoeu  2531  sb8mo  2533  cbvmo  2535  2euex  2573  2eu1  2582  bm1.1  2636  rmo5  3192  moeq  3415  funeu  5951  dffun8  5954  modom  8202  climmo  14332  rmoxfrdOLD  29459  rmoxfrd  29460  mont  32533  amosym1  32550  wl-sb8mot  33490  nexmo  34153  moxfr  37572