Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eupick | Unicode version |
Description: Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.) |
Ref | Expression |
---|---|
eupick |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eumo 1932 | . 2 | |
2 | mopick 1978 | . 2 | |
3 | 1, 2 | sylan 267 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wex 1381 weu 1900 wmo 1901 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 |
This theorem is referenced by: eupicka 1980 eupickb 1981 reupick 3221 reupick3 3222 copsexg 3981 eusv2nf 4188 funssres 4942 oprabid 5537 |
Copyright terms: Public domain | W3C validator |