Theorem snssg 4104

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 2474	. 2 |- ( x = A -> ( x e. B <-> A e. B ) )
2		sneq 3981	. . 3 |- ( x = A -> { x } = { A } )
3	2	sseq1d 3468	. 2 |- ( x = A -> ( { x } C_ B <-> { A } C_ B ) )
4		vex 3061	. . 3 |- x e. _V
5	4	snss 4095	. 2 |- ( x e. B <-> { x } C_ B )
6	1, 3, 5	vtoclbg 3117	1 |- ( A e. V -> ( A e. B <-> { A } C_ B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1405   e. wcel 1842   C_ wss 3413   {csn 3971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-v 3060  df-in 3420  df-ss 3427  df-sn 3972

This theorem is referenced by:  tppreqb  4112  snssi  4115  snssd  4116  prssg  4126  fvimacnvALT  5983  fr3nr  6596  vdwapid1  14700  acsfn  15271  cycsubg2  16560  cycsubg2cl  16561  pgpfac1lem1  17443  pgpfac1lem3a  17445  pgpfac1lem3  17446  pgpfac1lem5  17448  pgpfaclem2  17451  lspsnid  17957  lidldvgen  18221  isneip  19897  elnei  19903  iscnp4  20055  cnpnei  20056  nlly2i  20267  1stckgenlem  20344  flimopn  20766  flimclslem  20775  fclsneii  20808  fcfnei  20826  limcvallem  22565  ellimc2  22571  limcflf  22575  limccnp  22585  limccnp2  22586  limcco  22587  lhop2  22706  plyrem  22991  isppw  23767  h1did  26869  erdszelem8  29482  neibastop2  30576  prnc  31726  proot1mul  35500  islptre  36974