|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > eupick | Structured version Visualization version GIF 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 2577 | . 2 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | |
| 2 | mopick 2624 | . 2 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∃wex 1778 ∃*wmo 2537 ∃!weu 2567 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-12 2176 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-mo 2539 df-eu 2568 | 
| This theorem is referenced by: eupicka 2633 eupickb 2634 reupick 4328 reupick3 4329 eusv2nf 5394 reusv2lem3 5399 copsexgw 5494 copsexg 5495 funssres 6609 oprabidw 7463 oprabid 7464 txcn 23635 isch3 31261 bnj849 34940 iotasbc 44443 | 
| Copyright terms: Public domain | W3C validator |