Theorem snsssn

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

	Ref	Expression
Hypothesis	sneqr.1	⊢ 𝐴 ∈ V
Assertion	snsssn	⊢ ( { 𝐴 } ⊆ { 𝐵 } → 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sneqr.1	⊢ 𝐴 ∈ V
2		sssn	⊢ ( { 𝐴 } ⊆ { 𝐵 } ↔ ( { 𝐴 } = ∅ ∨ { 𝐴 } = { 𝐵 } ) )
3	1	snnz	⊢ { 𝐴 } ≠ ∅
4	3	neii	⊢ ¬ { 𝐴 } = ∅
5	4	pm2.21i	⊢ ( { 𝐴 } = ∅ → 𝐴 = 𝐵 )
6	1	sneqr	⊢ ( { 𝐴 } = { 𝐵 } → 𝐴 = 𝐵 )
7	5 6	jaoi	⊢ ( ( { 𝐴 } = ∅ ∨ { 𝐴 } = { 𝐵 } ) → 𝐴 = 𝐵 )
8	2 7	sylbi	⊢ ( { 𝐴 } ⊆ { 𝐵 } → 𝐴 = 𝐵 )