Theorem snssg 4105

Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)

Assertion

Ref	Expression
snssg	|- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Proof of Theorem snssg

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2517	. 2 |- ( x = A -> ( x e. B <-> A e. B ) )
2		sneq 3978	. . 3 |- ( x = A -> { x } = { A } )
3	2	sseq1d 3459	. 2 |- ( x = A -> ( { x } C_ B <-> { A } C_ B ) )
4		vex 3048	. . 3 |- x e. _V
5	4	snss 4096	. 2 |- ( x e. B <-> { x } C_ B )
6	1, 3, 5	vtoclbg 3108	1 |- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   e. wcel 1887   C_ wss 3404   {csn 3968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3047  df-in 3411  df-ss 3418  df-sn 3969

This theorem is referenced by:  tppreqb  4113  snssi  4116  snssd  4117  prssg  4127  fvimacnvALT  6001  fr3nr  6606  vdwapid1  14925  acsfn  15565  cycsubg2  16854  cycsubg2cl  16855  pgpfac1lem1  17707  pgpfac1lem3a  17709  pgpfac1lem3  17710  pgpfac1lem5  17712  pgpfaclem2  17715  lspsnid  18216  lidldvgen  18479  isneip  20121  elnei  20127  iscnp4  20279  cnpnei  20280  nlly2i  20491  1stckgenlem  20568  flimopn  20990  flimclslem  20999  fclsneii  21032  fcfnei  21050  limcvallem  22826  ellimc2  22832  limcflf  22836  limccnp  22846  limccnp2  22847  limcco  22848  lhop2  22967  plyrem  23258  isppw  24041  h1did  27204  erdszelem8  29921  neibastop2  31017  prnc  32300  proot1mul  36073  islptre  37699