This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in V \land \{A\} \subseteq \{B\}) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		sssn	$⊢ \{A\} \subseteq \{B\} \leftrightarrow (\{A\} = \emptyset \lor \{A\} = \{B\})$
2		snnzg	$⊢ A \in V \to \{A\} \neq \emptyset$
3	2	neneqd	$⊢ A \in V \to \neg \{A\} = \emptyset$
4	3	pm2.21d	$⊢ A \in V \to (\{A\} = \emptyset \to A = B)$
5		sneqrg	$⊢ A \in V \to (\{A\} = \{B\} \to A = B)$
6	4 5	jaod	$⊢ A \in V \to ((\{A\} = \emptyset \lor \{A\} = \{B\}) \to A = B)$
7	6	imp	$⊢ (A \in V \land (\{A\} = \emptyset \lor \{A\} = \{B\})) \to A = B$
8	1 7	sylan2b	$⊢ (A \in V \land \{A\} \subseteq \{B\}) \to A = B$