Theorem snssg 4012

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 2503	. 2 |- ( x = A -> ( x e. B <-> A e. B ) )
2		sneq 3892	. . 3 |- ( x = A -> { x } = { A } )
3	2	sseq1d 3388	. 2 |- ( x = A -> ( { x } C_ B <-> { A } C_ B ) )
4		vex 2980	. . 3 |- x e. _V
5	4	snss 4004	. 2 |- ( x e. B <-> { x } C_ B )
6	1, 3, 5	vtoclbg 3036	1 |- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   e. wcel 1756   C_ wss 3333   {csn 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2979  df-in 3340  df-ss 3347  df-sn 3883

This theorem is referenced by:  tppreqb  4019  snssi  4022  snssd  4023  prssg  4033  fvimacnvALT  5827  fr3nr  6396  vdwapid1  14041  acsfn  14602  cycsubg2  15723  cycsubg2cl  15724  pgpfac1lem1  16580  pgpfac1lem3a  16582  pgpfac1lem3  16583  pgpfac1lem5  16585  pgpfaclem2  16588  lspsnid  17079  lidldvgen  17342  isneip  18714  elnei  18720  iscnp4  18872  cnpnei  18873  nlly2i  19085  1stckgenlem  19131  flimopn  19553  flimclslem  19562  fclsneii  19595  fcfnei  19613  limcvallem  21351  ellimc2  21357  limcflf  21361  limccnp  21371  limccnp2  21372  limcco  21373  lhop2  21492  plyrem  21776  isppw  22457  h1did  24959  erdszelem8  27091  neibastop2  28587  prnc  28872  proot1mul  29569