Theorem snssi 4082

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
snssi	|- ( A e. B -> { A } C_ B )

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 4071	. 2 |- ( A e. B -> ( A e. B <-> { A } C_ B ) )
2	1	ibi 244	1 |- ( A e. B -> { A } C_ B )

Syntax hints:   -> wi 4   e. wcel 1872   C_ wss 3374   {csn 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-v 3019  df-in 3381  df-ss 3388  df-sn 3937

This theorem is referenced by:  difsnid  4084  pwpw0  4086  sssn  4096  ssunsn2  4097  tpssi  4104  pwsnALT  4152  snelpwi  4604  intid  4617  xpsspw  4905  djussxp  4937  dmressnsn  5100  fconst6g  5727  dffv2  5893  fvimacnvi  5950  fvimacnvALT  5955  fsn2  6016  fsnunf  6056  suceloni  6593  curry1  6838  curry2  6841  ressuppss  6884  ressuppssdif  6886  mapsn  7463  ralxpmap  7471  fodomr  7671  sucdom2  7716  en1eqsn  7749  enp1ilem  7753  findcard2  7759  findcard2s  7760  marypha1lem  7895  marypha2lem1  7897  epfrs  8162  dfac5lem4  8503  kmlem11  8536  ackbij1lem2  8597  fin23lem26  8701  isfin1-3  8762  hsmexlem4  8805  axdc3lem4  8829  axresscn  9518  nn0ssre  10819  xrsupss  11540  supxrmnf  11549  1fv  11854  1exp  12246  hashxrcl  12484  hashdifsn  12534  brfi1indlem  12592  snopiswrd  12624  repsdf2  12822  modfsummods  13791  fsum00  13796  incexc  13833  fprodsplit1f  13982  2ebits  14359  bitsinvp1  14361  lcmfunsnlem2lem1  14549  lcmfunsnlem2lem2  14550  lcmfunsnlem2  14551  coprmproddvdslem  14617  4sqlem19  14851  ramxrcl  14913  strlemor1  15155  mrcsncl  15456  acsfn1  15505  homaf  15863  dmcoass  15899  lubel  16306  gsumws1  16561  cycsubg2  16792  cntzsnval  16916  0frgp  17367  dpjidcl  17629  ablfac1eu  17644  lspsncl  18138  lspsnss  18151  lspsnid  18154  lpival  18407  lpiss  18412  lidldvgen  18417  znlidl  19041  frgpcyg  19081  frlmlbs  19292  mat1dimelbas  19433  mat1dimmul  19438  smadiadetglem2  19634  isneip  20058  neips  20066  opnneip  20072  maxlp  20100  restsn2  20124  leordtval2  20165  ist1-3  20302  ordtt1  20332  2ndcdisj2  20409  uffix  20873  neiflim  20926  ptcmplem5  21008  cnextfres1  21020  haustsms2  21088  ust0  21171  ustuqtop5  21197  dscopn  21525  icccmplem1  21777  bndth  21923  ovolsn  22385  icombl1  22453  plyun0  23088  coeeulem  23115  coeeu  23116  vieta1lem2  23201  aalioulem2  23226  taylfval  23251  perfectlem2  24095  istrkg2ld  24445  axlowdimlem7  24915  axlowdimlem10  24918  konigsberg  25652  hsn0elch  26838  chsupsn  27003  chsup0  27138  h1deoi  27139  h1dei  27140  h1did  27141  h1de2ctlem  27145  h1de2ci  27146  spansni  27147  spansnch  27150  elspansncl  27155  spansnpji  27168  spanunsni  27169  spanpr  27170  h1datomi  27171  spansnji  27236  h1da  27939  atom1d  27943  superpos  27944  disjun0  28146  esumnul  28816  esumcst  28831  hashf2  28852  esum2d  28861  measvuni  28983  cntnevol  28997  eulerpartlemt  29151  eulerpartlemmf  29155  eulerpartlemgh  29158  ballotlemfp1  29271  dfon2lem3  30377  altxpsspw  30688  bj-snglss  31475  poimirlem16  31863  poimirlem19  31866  poimirlem23  31870  poimirlem25  31872  poimirlem26  31873  poimirlem29  31876  poimirlem31  31878  mblfinlem2  31885  dvasin  31935  fdc  31981  prnc  32207  isfldidl  32208  ispridlc  32210  islshpsm  32458  snatpsubN  33227  polatN  33408  atpsubclN  33422  pclfinclN  33427  mapfzcons  35470  mzpcompact2lem  35505  diophrw  35513  brfvidRP  36193  cotrcltrcl  36230  corcltrcl  36244  cotrclrcl  36247  binomcxplemnotnn0  36618  snelpwrVD  37143  disjiun2  37314  mccllem  37560  islptre  37582  cncfdmsn  37651  snmbl  37723  stoweidlem44  37788  sge0tsms  38073  sge0iunmptlemfi  38106  ismeannd  38156  isomenndlem  38202  hoidmvlelem3  38266  hoidmvlelem4  38267  ovnhoilem1  38270  fnbrafvb  38469  afvres  38487  perfectALTVlem2  38657  nnsum3primesprm  38698  mapsnop  39719  lincext2  39841  snlindsntorlem  39856  aacllem  40133