Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Definition df-mo 1381

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 1399. For other possible definitions see mo2 1398 and mo4 1401.

Assertion

Ref	Expression
df-mo

---

Detailed syntax breakdown of Definition df-mo

Step	Hyp	Ref	Expression
1		wph	. . 3
2		vx	. . 3
3	1, 2	wmo 1379	. 2
4	1, 2	wex 978	. . 3
5	1, 2	weu 1378	. . 3
6	4, 5	wi 3	. 2
7	3, 6	wb 146	1

Colors of variables: wff set class

This definition is referenced by:  mo2 1398  mobid 1402  hbmo1 1404  hbmo 1405  cbvmo 1406  exmoeu 1411  moabs 1413  exmo 1414  moeq 1916

Copyright terms: Public domain