| 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 2608 | . 2 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | |
| 2 | mopick 2655 | . 2 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) | |
| 3 | 1, 2 | sylan 592 | 1 ⊢ ((∃!𝑥𝜑 ∧ ∃𝑥(𝜑 ∧ 𝜓)) → (𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∃wex 1812 ∃*wmo 2567 ∃!weu 2598 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-12 2216 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-mo 2569 df-eu 2599 |
| This theorem is used by: eupicka 2664 eupickb 2665 reupick 4282 reupick3 4283 eusv2nf 5368 reusv2lem3 5373 copsexgw 5474 copsexgwOLD 5475 copsexg 5476 funssres 6584 oprabidw 7447 oprabid 7448 txcn 23812 isch3 31622 bnj849 35337 iotasbc 45162 |
| Copyright terms: Public domain | W3C validator |