Definition df-mo 2474

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

This definition is referenced by:  mo2v  2476  nfmo1  2480  nfmod2  2482  mobid  2488  exmo  2494  eu5  2495  moabs  2500  exmoeu  2501  sb8mo  2503  cbvmo  2505  2euex  2543  2eu1  2552  bm1.1  2606  rmo5  3155  moeq  3369  funeu  5882  dffun8  5885  modom  8121  climmo  14238  rmoxfrdOLD  29221  rmoxfrd  29222  mont  32103  amosym1  32120  wl-sb8mot  33031  moxfr  36774