| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define "there exists
at most one |
| Ref | Expression |
|---|---|
| df-mo |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph |
. . 3
| |
| 2 | vx |
. . 3
| |
| 3 | 1, 2 | wmo 1381 |
. 2
|
| 4 | 1, 2 | wex 980 |
. . 3
|
| 5 | 1, 2 | weu 1380 |
. . 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 1400 mobid 1404 hbmo1 1406 hbmo 1407 cbvmo 1408 exmoeu 1413 moabs 1415 exmo 1416 moeq 1920 |