Description: Nested at-most-one and unique existential quantifiers. (Contributed by NM, 25-Jan-2006) (Proof shortened by Wolf Lammen, 27-Dec-2018)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | moaneu | |- E* x ( ph /\ E! x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moanmo | |- E* x ( ph /\ E* x ph ) |
|
| 2 | eumo | |- ( E! x ph -> E* x ph ) |
|
| 3 | 2 | anim2i | |- ( ( ph /\ E! x ph ) -> ( ph /\ E* x ph ) ) |
| 4 | 3 | moimi | |- ( E* x ( ph /\ E* x ph ) -> E* x ( ph /\ E! x ph ) ) |
| 5 | 1 4 | ax-mp | |- E* x ( ph /\ E! x ph ) |