Theorem snssg 4166

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 2539	. 2 |- ( x = A -> ( x e. B <-> A e. B ) )
2		sneq 4043	. . 3 |- ( x = A -> { x } = { A } )
3	2	sseq1d 3536	. 2 |- ( x = A -> ( { x } C_ B <-> { A } C_ B ) )
4		vex 3121	. . 3 |- x e. _V
5	4	snss 4157	. 2 |- ( x e. B <-> { x } C_ B )
6	1, 3, 5	vtoclbg 3177	1 |- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   C_ wss 3481   {csn 4033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-v 3120  df-in 3488  df-ss 3495  df-sn 4034

This theorem is referenced by:  tppreqb  4174  snssi  4177  snssd  4178  prssg  4188  fvimacnvALT  6007  fr3nr  6610  vdwapid1  14369  acsfn  14931  cycsubg2  16110  cycsubg2cl  16111  pgpfac1lem1  16997  pgpfac1lem3a  16999  pgpfac1lem3  17000  pgpfac1lem5  17002  pgpfaclem2  17005  lspsnid  17510  lidldvgen  17773  isneip  19474  elnei  19480  iscnp4  19632  cnpnei  19633  nlly2i  19845  1stckgenlem  19922  flimopn  20344  flimclslem  20353  fclsneii  20386  fcfnei  20404  limcvallem  22143  ellimc2  22149  limcflf  22153  limccnp  22163  limccnp2  22164  limcco  22165  lhop2  22284  plyrem  22568  isppw  23254  h1did  26292  erdszelem8  28467  neibastop2  30106  prnc  30391  proot1mul  31085  islptre  31484