| 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 2609 | . 2 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | |
| 2 | mopick 2656 | . 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 2568 ∃!weu 2599 |
| 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 2570 df-eu 2600 |
| This theorem is used by: eupicka 2665 eupickb 2666 reupick 4285 reupick3 4286 eusv2nf 5371 reusv2lem3 5376 copsexgw 5477 copsexgwOLD 5478 copsexg 5479 funssres 6587 oprabidw 7454 oprabid 7455 txcn 23820 isch3 31630 bnj849 35345 iotasbc 45170 |
| Copyright terms: Public domain | W3C validator |