Metamath Proof Explorer


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 AVABAB

Proof

Step Hyp Ref Expression
1 velsn xAx=A
2 1 imbi1i xAxBx=AxB
3 2 albii xxAxBxx=AxB
4 3 a1i AVxxAxBxx=AxB
5 dfss2 ABxxAxB
6 5 a1i AVABxxAxB
7 clel2g AVABxx=AxB
8 4 6 7 3bitr4rd AVABAB