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

Proof

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