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	$$⊢A\in B\to \left\{A\right\}\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
2		eleq1a	$$⊢A\in B\to \left(x=A\to x\in B\right)$$
3	1 2	biimtrid	$$⊢A\in B\to \left(x\in \left\{A\right\}\to x\in B\right)$$
4	3	alrimiv	$$⊢A\in B\to \forall x\left(x\in \left\{A\right\}\to x\in B\right)$$
5		df-ss	$$⊢\left\{A\right\}\subseteq B\leftrightarrow \forall x\left(x\in \left\{A\right\}\to x\in B\right)$$
6	4 5	sylibr	$$⊢A\in B\to \left\{A\right\}\subseteq B$$