Metamath Proof Explorer


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 ABAB

Proof

Step Hyp Ref Expression
1 velsn xAx=A
2 eleq1a ABx=AxB
3 1 2 syl5bi ABxAxB
4 3 alrimiv ABxxAxB
5 dfss2 ABxxAxB
6 4 5 sylibr ABAB