Theorem snssgOLD

Description: Obsolete version of snssgOLD as of 1-Jan-2025. (Contributed by NM, 22-Jul-2001) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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