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	|- ( ( A e. V /\ { A } C_ { B } ) -> A = B )

Proof

Step	Hyp	Ref	Expression
1		sssn	|- ( { A } C_ { B } <-> ( { A } = (/) \/ { A } = { B } ) )
2		snnzg	|- ( A e. V -> { A } =/= (/) )
3	2	neneqd	|- ( A e. V -> -. { A } = (/) )
4	3	pm2.21d	|- ( A e. V -> ( { A } = (/) -> A = B ) )
5		sneqrg	|- ( A e. V -> ( { A } = { B } -> A = B ) )
6	4 5	jaod	|- ( A e. V -> ( ( { A } = (/) \/ { A } = { B } ) -> A = B ) )
7	6	imp	|- ( ( A e. V /\ ( { A } = (/) \/ { A } = { B } ) ) -> A = B )
8	1 7	sylan2b	|- ( ( A e. V /\ { A } C_ { B } ) -> A = B )