Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eu5 | GIF version |
Description: Uniqueness in terms of "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.) |
Ref | Expression |
---|---|
eu5 | ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | euex 2049 | . . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) | |
2 | eumo 2051 | . . 3 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | |
3 | 1, 2 | jca 304 | . 2 ⊢ (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
4 | df-mo 2023 | . . . . 5 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
5 | 4 | biimpi 119 | . . . 4 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑)) |
6 | 5 | imp 123 | . . 3 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥𝜑) → ∃!𝑥𝜑) |
7 | 6 | ancoms 266 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → ∃!𝑥𝜑) |
8 | 3, 7 | impbii 125 | 1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∃wex 1485 ∃!weu 2019 ∃*wmo 2020 |
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 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 |
This theorem is referenced by: exmoeu2 2067 euan 2075 eu4 2081 euim 2087 euexex 2104 2euex 2106 2euswapdc 2110 2exeu 2111 reu5 2682 reuss2 3407 funcnv3 5260 fnres 5314 fnopabg 5321 brprcneu 5489 dff3im 5641 recmulnqg 7353 uptx 13068 |
Copyright terms: Public domain | W3C validator |