Theorem mosssn

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

	Ref	Expression
Assertion	mosssn	⊢ ( 𝐴 ⊆ { 𝐵 } → ∃* 𝑥 𝑥 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sssn	⊢ ( 𝐴 ⊆ { 𝐵 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )
2		mo0	⊢ ( 𝐴 = ∅ → ∃* 𝑥 𝑥 ∈ 𝐴 )
3		mosn	⊢ ( 𝐴 = { 𝐵 } → ∃* 𝑥 𝑥 ∈ 𝐴 )
4	2 3	jaoi	⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) → ∃* 𝑥 𝑥 ∈ 𝐴 )
5	1 4	sylbi	⊢ ( 𝐴 ⊆ { 𝐵 } → ∃* 𝑥 𝑥 ∈ 𝐴 )