Theorem snssi 4038

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 4028	. 2 |- ( A e. B -> ( A e. B <-> { A } C_ B ) )
2	1	ibi 241	1 |- ( A e. B -> { A } C_ B )

Syntax hints:   -> wi 4   e. wcel 1756   C_ wss 3349   {csn 3898

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 2995  df-in 3356  df-ss 3363  df-sn 3899

This theorem is referenced by:  difsnid  4040  pwpw0  4042  sssn  4052  ssunsn2  4053  tpssi  4060  pwsnALT  4107  snelpwi  4558  intid  4571  xpsspw  4974  xpsspwOLD  4975  djussxp  5006  xpimasnOLD  5305  fconst6g  5620  dffv2  5785  fvimacnvi  5838  fvimacnvALT  5843  fsn2  5904  fsnunf  5937  suceloni  6445  curry1  6685  curry2  6688  ressuppss  6729  ressuppssdif  6731  mapsn  7275  ralxpmap  7283  fodomr  7483  sucdom2  7528  en1eqsn  7563  enp1ilem  7567  findcard2  7573  findcard2s  7574  marypha1lem  7704  marypha2lem1  7706  epfrs  7972  dfac5lem4  8317  kmlem11  8350  ackbij1lem2  8411  fin23lem26  8515  isfin1-3  8576  hsmexlem4  8619  axdc3lem4  8643  axresscn  9336  nn0ssre  10604  xrsupss  11292  supxrmnf  11301  1fv  11553  1exp  11914  hashxrcl  12148  hashdifsn  12190  brfi1indlem  12239  snopiswrd  12264  repsdf2  12437  fsum00  13282  incexc  13321  xpnnenOLD  13513  2ebits  13664  bitsinvp1  13666  4sqlem19  14045  ramxrcl  14099  strlemor1  14286  mrcsncl  14571  acsfn1  14620  homaf  14919  dmcoass  14955  lubel  15313  gsumws1  15538  cycsubg2  15739  cntzsnval  15863  0frgp  16297  dpjidcl  16579  dpjidclOLD  16586  ablfac1eu  16596  lspsncl  17080  lspsnss  17093  lspsnid  17096  lpival  17349  lpiss  17354  lidldvgen  17359  znlidl  17986  znlidlOLD  17990  frgpcyg  18028  frlmlbs  18247  smadiadetglem2  18500  isneip  18731  neips  18739  opnneip  18745  maxlp  18773  restsn2  18797  leordtval2  18838  ist1-3  18975  ordtt1  19005  2ndcdisj2  19083  uffix  19516  neiflim  19569  ptcmplem5  19650  cnextfres  19662  haustsms2  19729  ust0  19816  ustuqtop5  19842  dscopn  20188  icccmplem1  20421  bndth  20552  ovolsn  21000  icombl1  21066  plyun0  21687  coeeulem  21714  coeeu  21715  vieta1lem2  21799  aalioulem2  21821  taylfval  21846  perfectlem2  22591  axlowdimlem7  23216  axlowdimlem10  23219  konigsberg  23630  hsn0elch  24673  chsupsn  24838  chsup0  24973  h1deoi  24974  h1dei  24975  h1did  24976  h1de2ctlem  24980  h1de2ci  24981  spansni  24982  spansnch  24985  elspansncl  24990  spansnpji  25003  spanunsni  25004  spanpr  25005  h1datomi  25006  spansnji  25071  h1da  25775  atom1d  25779  superpos  25780  resf1o  26052  esumnul  26524  esumcst  26536  hashf2  26555  measvuni  26650  cntnevol  26664  eulerpartlemt  26776  eulerpartlemmf  26780  eulerpartlemgh  26783  ballotlemfp1  26896  dfon2lem3  27620  altxpsspw  28030  mblfinlem2  28455  dvasin  28506  fdc  28667  prnc  28893  isfldidl  28894  ispridlc  28896  mapfzcons  29078  mzpcompact2lem  29114  diophrw  29123  stoweidlem44  29865  dmressnsn  30054  fnbrafvb  30086  afvres  30104  modfsummods  30270  mapsnop  30762  mat1dimelbas  30906  mat1dimmul  30911  lincext2  30986  snlindsntorlem  31001  snelpwrVD  31663  bj-snglss  32559  islshpsm  32721  snatpsubN  33490  polatN  33671  atpsubclN  33685  pclfinclN  33690