Theorem snssb

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

	Ref	Expression
Assertion	snssb	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ss	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
2		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
3	2	imbi1i	⊢ ( ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
4	3	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
5		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
6	5	pm5.74i	⊢ ( ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
7	6	albii	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
8		19.23v	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) )
9		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
10	9	bicomi	⊢ ( ∃ 𝑥 𝑥 = 𝐴 ↔ 𝐴 ∈ V )
11	10	imbi1i	⊢ ( ( ∃ 𝑥 𝑥 = 𝐴 → 𝐴 ∈ 𝐵 ) ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )
12	7 8 11	3bitri	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )
13	1 4 12	3bitri	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ( 𝐴 ∈ V → 𝐴 ∈ 𝐵 ) )