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

Metamath Proof Explorer

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	$⊢ A \in V$
	Assertion	snsssn	$⊢ \{A\} \subseteq \{B\} \to A = B$

Step	Hyp	Ref	Expression
1		sneqr.1	$⊢ A \in V$
2		sssn	$⊢ \{A\} \subseteq \{B\} \leftrightarrow (\{A\} = \emptyset \lor \{A\} = \{B\})$
3	1	snnz	$⊢ \{A\} \neq \emptyset$
4	3	neii	$⊢ \neg \{A\} = \emptyset$
5	4	pm2.21i	$⊢ \{A\} = \emptyset \to A = B$
6	1	sneqr	$⊢ \{A\} = \{B\} \to A = B$
7	5 6	jaoi	$⊢ (\{A\} = \emptyset \lor \{A\} = \{B\}) \to A = B$
8	2 7	sylbi	$⊢ \{A\} \subseteq \{B\} \to A = B$