![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > df-eu | Unicode version |
Description: Define existential
uniqueness, i.e. "there exists exactly one
such that ." Definition
10.1 of [BellMachover] p. 97; also
Definition *14.02 of [WhiteheadRussell] p. 175. Other
possible
definitions are given by eu1 2327, eu2 2326, eu3v 2312,
and eu5 2310 (which in
some cases we show with a hypothesis -> A. in place of a
distinct variable condition on and ). Double uniqueness is
tricky: does not mean
"exactly one and one
" (see 2eu4 2380). (Contributed by NM,
12-Aug-1993.) |
Ref | Expression |
---|---|
df-eu |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 | |
2 | vx | . . 3 | |
3 | 1, 2 | weu 2282 | . 2 |
4 | vy | . . . . . 6 | |
5 | 2, 4 | weq 1733 | . . . . 5 |
6 | 1, 5 | wb 184 | . . . 4 |
7 | 6, 2 | wal 1393 | . . 3 |
8 | 7, 4 | wex 1612 | . 2 |
9 | 3, 8 | wb 184 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: euequ1 2288 mo2v 2289 mo2vOLD 2290 mo2vOLDOLD 2291 euf 2292 nfeu1 2294 nfeud2 2296 eubid 2302 euex 2308 sb8eu 2318 sb8euOLD 2319 exists1 2388 reu6 3288 euabsn2 4101 euotd 4753 iotauni 5568 iota1 5570 iotanul 5571 iotaex 5573 iota4 5574 fv3 5884 eufnfv 6146 seqomlem2 7135 aceq1 8519 dfac5 8530 wl-sb8eut 30022 iotain 31324 iotaexeu 31325 iotasbc 31326 iotavalsb 31340 sbiota1 31341 bnj89 33774 |
Copyright terms: Public domain | W3C validator |