Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > euex | GIF version |
Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
euex | ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1506 | . . 3 ⊢ (𝜑 → ∀𝑦𝜑) | |
2 | 1 | eu1 2022 | . 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) |
3 | exsimpl 1596 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)) → ∃𝑥𝜑) | |
4 | 2, 3 | sylbi 120 | 1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∀wal 1329 ∃wex 1468 [wsb 1735 ∃!weu 1997 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-eu 2000 |
This theorem is referenced by: eu2 2041 eu3h 2042 eu5 2044 exmoeudc 2060 eupickbi 2079 2eu2ex 2086 euxfrdc 2865 repizf 4039 eusvnf 4369 eusvnfb 4370 tz6.12c 5444 ndmfvg 5445 nfvres 5447 0fv 5449 eusvobj2 5753 fnoprabg 5865 txcn 12433 |
Copyright terms: Public domain | W3C validator |