Definition df-mo 2475

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

This definition is referenced by:  mo2v  2477  nfmo1  2481  nfmod2  2483  mobid  2489  exmo  2495  eu5  2496  moabs  2501  exmoeu  2502  sb8mo  2504  cbvmo  2506  2euex  2544  2eu1  2553  bm1.1  2607  rmo5  3162  moeq  3382  funeu  5913  dffun8  5916  modom  8161  climmo  14288  rmoxfrdOLD  29332  rmoxfrd  29333  mont  32408  amosym1  32425  wl-sb8mot  33360  nexmo  34011  moxfr  37255