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

Metamath Proof Explorer

Theorem mosn

Description: "At most one" element in a singleton. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mosn ⊢ A = B → ∃* x x ∈ A

Proof

Step Hyp Ref Expression
1 rmosn ⊢ ∃* x ∈ B ⊤
2 rmotru ⊢ ∃* x x ∈ B ↔ ∃* x ∈ B ⊤
3 1 2 mpbir ⊢ ∃* x x ∈ B
4 eleq2 ⊢ A = B → x ∈ A ↔ x ∈ B
5 4 mobidv ⊢ A = B → ∃* x x ∈ A ↔ ∃* x x ∈ B
6 3 5 mpbiri ⊢ A = B → ∃* x x ∈ A