New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 2244 | . 2 | |
2 | mopick 2266 | . 2 | |
3 | 1, 2 | sylan 457 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 wex 1541 weu 2204 wmo 2205 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 |
This theorem is referenced by: eupicka 2268 eupickb 2269 reupick 3539 reupick3 3540 copsexg 4607 funssres 5144 oprabid 5550 |
Copyright terms: Public domain | W3C validator |