snssb

Description: Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025)

		Ref	Expression
	Assertion	snssb	$⊢ \{A\} \subseteq B \leftrightarrow (A \in V \to A \in B)$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ \{A\} \subseteq B \leftrightarrow \forall x (x \in \{A\} \to x \in B)$
2		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
3	2	imbi1i	$⊢ (x \in \{A\} \to x \in B) \leftrightarrow (x = A \to x \in B)$
4	3	albii	$⊢ \forall x (x \in \{A\} \to x \in B) \leftrightarrow \forall x (x = A \to x \in B)$
5		eleq1	$⊢ x = A \to (x \in B \leftrightarrow A \in B)$
6	5	pm5.74i	$⊢ (x = A \to x \in B) \leftrightarrow (x = A \to A \in B)$
7	6	albii	$⊢ \forall x (x = A \to x \in B) \leftrightarrow \forall x (x = A \to A \in B)$
8		19.23v	$⊢ \forall x (x = A \to A \in B) \leftrightarrow (\exists x x = A \to A \in B)$
9		isset	$⊢ A \in V \leftrightarrow \exists x x = A$
10	9	bicomi	$⊢ \exists x x = A \leftrightarrow A \in V$
11	10	imbi1i	$⊢ (\exists x x = A \to A \in B) \leftrightarrow (A \in V \to A \in B)$
12	7 8 11	3bitri	$⊢ \forall x (x = A \to x \in B) \leftrightarrow (A \in V \to A \in B)$
13	1 4 12	3bitri	$⊢ \{A\} \subseteq B \leftrightarrow (A \in V \to A \in B)$

Metamath Proof Explorer