Description: Existence is equivalent to uniqueness implying existential uniqueness. (Contributed by NM, 5-Apr-2004) (Proof shortened by Wolf Lammen, 5-Dec-2018) (Proof shortened by BJ, 7-Oct-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | exmoeu | |- ( E. x ph <-> ( E* x ph -> E! x ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exmoeub | |- ( E. x ph -> ( E* x ph <-> E! x ph ) ) |
|
| 2 | 1 | biimpd | |- ( E. x ph -> ( E* x ph -> E! x ph ) ) |
| 3 | nexmo | |- ( -. E. x ph -> E* x ph ) |
|
| 4 | 3 | con1i | |- ( -. E* x ph -> E. x ph ) |
| 5 | euex | |- ( E! x ph -> E. x ph ) |
|
| 6 | 4 5 | ja | |- ( ( E* x ph -> E! x ph ) -> E. x ph ) |
| 7 | 2 6 | impbii | |- ( E. x ph <-> ( E* x ph -> E! x ph ) ) |