Theorem mosn

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

	Ref	Expression
Assertion	mosn	⊢ ( 𝐴 = { 𝐵 } → ∃* 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rmosn	⊢ ∃* 𝑥 ∈ { 𝐵 } ⊤
2		rmotru	⊢ ( ∃* 𝑥 𝑥 ∈ { 𝐵 } ↔ ∃* 𝑥 ∈ { 𝐵 } ⊤ )
3	1 2	mpbir	⊢ ∃* 𝑥 𝑥 ∈ { 𝐵 }
4		eleq2	⊢ ( 𝐴 = { 𝐵 } → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝐵 } ) )
5	4	mobidv	⊢ ( 𝐴 = { 𝐵 } → ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∃* 𝑥 𝑥 ∈ { 𝐵 } ) )
6	3 5	mpbiri	⊢ ( 𝐴 = { 𝐵 } → ∃* 𝑥 𝑥 ∈ 𝐴 )