Theorem snssiALT

Description: If a class is an element of another class, then its singleton is a subclass of that other class. Alternate proof of snssi . This theorem was automatically generated from snssiALTVD using a translation program. (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snssiALT	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
2		eleq1a	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
3	1 2	biimtrid	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
4	3	alrimiv	⊢ ( 𝐴 ∈ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
5		df-ss	⊢ ( { 𝐴 } ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝐴 } → 𝑥 ∈ 𝐵 ) )
6	4 5	sylibr	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ⊆ 𝐵 )