This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rmoeq

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 ⊢ ∃* x ∈ B x = A

Proof

Step Hyp Ref Expression
1 moeq ⊢ ∃* x x = A
2 1 moani ⊢ ∃* x x ∈ B ∧ x = A
3 df-rmo ⊢ ∃* x ∈ B x = A ↔ ∃* x x ∈ B ∧ x = A
4 2 3 mpbir ⊢ ∃* x ∈ B x = A