Theorem snsssng

Description: If a singleton is a subset of another, their members are equal. (Contributed by NM, 28-May-2006) (Revised by Thierry Arnoux, 11-Apr-2024)

	Ref	Expression
Assertion	snsssng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝐴 } ⊆ { 𝐵 } ) → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sssn	⊢ ( { 𝐴 } ⊆ { 𝐵 } ↔ ( { 𝐴 } = ∅ ∨ { 𝐴 } = { 𝐵 } ) )
2		snnzg	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≠ ∅ )
3	2	neneqd	⊢ ( 𝐴 ∈ 𝑉 → ¬ { 𝐴 } = ∅ )
4	3	pm2.21d	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = ∅ → 𝐴 = 𝐵 ) )
5		sneqrg	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } → 𝐴 = 𝐵 ) )
6	4 5	jaod	⊢ ( 𝐴 ∈ 𝑉 → ( ( { 𝐴 } = ∅ ∨ { 𝐴 } = { 𝐵 } ) → 𝐴 = 𝐵 ) )
7	6	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( { 𝐴 } = ∅ ∨ { 𝐴 } = { 𝐵 } ) ) → 𝐴 = 𝐵 )
8	1 7	sylan2b	⊢ ( ( 𝐴 ∈ 𝑉 ∧ { 𝐴 } ⊆ { 𝐵 } ) → 𝐴 = 𝐵 )