Theorem snssb

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

	Ref	Expression
Assertion	snssb	|- ( { A } C_ B <-> ( A e. _V -> A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		df-ss	|- ( { A } C_ B <-> A. x ( x e. { A } -> x e. B ) )
2		velsn	|- ( x e. { A } <-> x = A )
3	2	imbi1i	|- ( ( x e. { A } -> x e. B ) <-> ( x = A -> x e. B ) )
4	3	albii	|- ( A. x ( x e. { A } -> x e. B ) <-> A. x ( x = A -> x e. B ) )
5		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
6	5	pm5.74i	|- ( ( x = A -> x e. B ) <-> ( x = A -> A e. B ) )
7	6	albii	|- ( A. x ( x = A -> x e. B ) <-> A. x ( x = A -> A e. B ) )
8		19.23v	|- ( A. x ( x = A -> A e. B ) <-> ( E. x x = A -> A e. B ) )
9		isset	|- ( A e. _V <-> E. x x = A )
10	9	bicomi	|- ( E. x x = A <-> A e. _V )
11	10	imbi1i	|- ( ( E. x x = A -> A e. B ) <-> ( A e. _V -> A e. B ) )
12	7 8 11	3bitri	|- ( A. x ( x = A -> x e. B ) <-> ( A e. _V -> A e. B ) )
13	1 4 12	3bitri	|- ( { A } C_ B <-> ( A e. _V -> A e. B ) )