Theorem snssg

Description: The singleton of an element of a class is a subset of the class (general form of snss ). Theorem 7.4 of Quine p. 49. (Contributed by NM, 22-Jul-2001)

	Ref	Expression
Assertion	snssg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
2	1	imbi1i	⊢ ( ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
3	2	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
4	3	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ) )
5		dfss2	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
6	5	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) ) )
7		clel2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) ) )
8	4 6 7	3bitr4rd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝐵 ↔ { 𝐴 } ⊆ 𝐵 ) )