Theorem mosssn2

Description: Two ways of expressing "at most one" element in a class. (Contributed by Zhi Wang, 23-Sep-2024)

	Ref	Expression
Assertion	mosssn2	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 𝐴 ⊆ { 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		19.45v	⊢ ( ∃ 𝑦 ( 𝐴 = ∅ ∨ 𝐴 = { 𝑦 } ) ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )
2		sssn	⊢ ( 𝐴 ⊆ { 𝑦 } ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝑦 } ) )
3	2	exbii	⊢ ( ∃ 𝑦 𝐴 ⊆ { 𝑦 } ↔ ∃ 𝑦 ( 𝐴 = ∅ ∨ 𝐴 = { 𝑦 } ) )
4		mo0sn	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑦 𝐴 = { 𝑦 } ) )
5	1 3 4	3bitr4ri	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 𝐴 ⊆ { 𝑦 } )