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 1971 | . . 3 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) | |
2 | eumo 1973 | . . 3 ⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | |
3 | 1, 2 | jca 300 | . 2 ⊢ (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
4 | df-mo 1945 | . . . . 5 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | |
5 | 4 | biimpi 118 | . . . 4 ⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑)) |
6 | 5 | imp 122 | . . 3 ⊢ ((∃*𝑥𝜑 ∧ ∃𝑥𝜑) → ∃!𝑥𝜑) |
7 | 6 | ancoms 264 | . 2 ⊢ ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → ∃!𝑥𝜑) |
8 | 3, 7 | impbii 124 | 1 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∃wex 1421 ∃!weu 1941 ∃*wmo 1942 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 |
This theorem is referenced by: exmoeu2 1989 euan 1997 eu4 2003 euim 2009 euexex 2026 2euex 2028 2euswapdc 2032 2exeu 2033 reu5 2566 reuss2 3244 funcnv3 4981 fnres 5035 fnopabg 5042 brprcneu 5191 dff3im 5333 recmulnqg 6581 |
Copyright terms: Public domain | W3C validator |