Description: Equality's restricted existential "at most one" property. (Contributed by Thierry Arnoux, 30-Mar-2018) (Revised by AV, 27-Oct-2020) (Proof shortened by NM, 29-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rmoeq | |- E* x e. B x = A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | moeq | |- E* x x = A |
|
| 2 | 1 | moani | |- E* x ( x e. B /\ x = A ) |
| 3 | df-rmo | |- ( E* x e. B x = A <-> E* x ( x e. B /\ x = A ) ) |
|
| 4 | 2 3 | mpbir | |- E* x e. B x = A |