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 ∃* 𝑥𝐵 𝑥 = 𝐴

Proof

Step Hyp Ref Expression
1 moeq ∃* 𝑥 𝑥 = 𝐴
2 1 moani ∃* 𝑥 ( 𝑥𝐵𝑥 = 𝐴 )
3 df-rmo ( ∃* 𝑥𝐵 𝑥 = 𝐴 ↔ ∃* 𝑥 ( 𝑥𝐵𝑥 = 𝐴 ) )
4 2 3 mpbir ∃* 𝑥𝐵 𝑥 = 𝐴