Theorem snssi 4171

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 4160	. 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 1767   C_ wss 3476   {csn 4027

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 3115  df-in 3483  df-ss 3490  df-sn 4028

This theorem is referenced by:  difsnid  4173  pwpw0  4175  sssn  4185  ssunsn2  4186  tpssi  4193  pwsnALT  4240  snelpwi  4692  intid  4705  xpsspw  5116  xpsspwOLD  5117  djussxp  5148  dmressnsn  5312  xpimasnOLD  5453  fconst6g  5774  dffv2  5941  fvimacnvi  5996  fvimacnvALT  6001  fsn2  6062  fsnunf  6100  suceloni  6633  curry1  6876  curry2  6879  ressuppss  6920  ressuppssdif  6922  mapsn  7461  ralxpmap  7469  fodomr  7669  sucdom2  7715  en1eqsn  7750  enp1ilem  7755  findcard2  7761  findcard2s  7762  marypha1lem  7894  marypha2lem1  7896  epfrs  8163  dfac5lem4  8508  kmlem11  8541  ackbij1lem2  8602  fin23lem26  8706  isfin1-3  8767  hsmexlem4  8810  axdc3lem4  8834  axresscn  9526  nn0ssre  10800  xrsupss  11501  supxrmnf  11510  1fv  11790  1exp  12164  hashxrcl  12398  hashdifsn  12443  brfi1indlem  12498  snopiswrd  12523  repsdf2  12716  modfsummods  13573  fsum00  13578  incexc  13615  xpnnenOLD  13807  2ebits  13959  bitsinvp1  13961  4sqlem19  14343  ramxrcl  14397  strlemor1  14585  mrcsncl  14870  acsfn1  14919  homaf  15218  dmcoass  15254  lubel  15612  gsumws1  15842  cycsubg2  16052  cntzsnval  16176  0frgp  16612  dpjidcl  16921  dpjidclOLD  16928  ablfac1eu  16938  lspsncl  17435  lspsnss  17448  lspsnid  17451  lpival  17704  lpiss  17709  lidldvgen  17714  znlidl  18377  znlidlOLD  18381  frgpcyg  18419  frlmlbs  18638  mat1dimelbas  18780  mat1dimmul  18785  smadiadetglem2  18981  isneip  19412  neips  19420  opnneip  19426  maxlp  19454  restsn2  19478  leordtval2  19519  ist1-3  19656  ordtt1  19686  2ndcdisj2  19764  uffix  20249  neiflim  20302  ptcmplem5  20383  cnextfres  20395  haustsms2  20462  ust0  20549  ustuqtop5  20575  dscopn  20921  icccmplem1  21154  bndth  21285  ovolsn  21733  icombl1  21800  plyun0  22421  coeeulem  22448  coeeu  22449  vieta1lem2  22533  aalioulem2  22555  taylfval  22580  perfectlem2  23330  istrkg2ld  23683  axlowdimlem7  24024  axlowdimlem10  24027  konigsberg  24760  hsn0elch  25939  chsupsn  26104  chsup0  26239  h1deoi  26240  h1dei  26241  h1did  26242  h1de2ctlem  26246  h1de2ci  26247  spansni  26248  spansnch  26251  elspansncl  26256  spansnpji  26269  spanunsni  26270  spanpr  26271  h1datomi  26272  spansnji  26337  h1da  27041  atom1d  27045  superpos  27046  resf1o  27322  esumnul  27810  esumcst  27822  hashf2  27841  measvuni  27936  cntnevol  27950  eulerpartlemt  28061  eulerpartlemmf  28065  eulerpartlemgh  28068  ballotlemfp1  28181  dfon2lem3  29070  altxpsspw  29480  mblfinlem2  29905  dvasin  29956  fdc  30068  prnc  30294  isfldidl  30295  ispridlc  30297  mapfzcons  30479  mzpcompact2lem  30515  diophrw  30523  islptre  31388  cncfdmsn  31456  snmbl  31508  stoweidlem44  31571  fnbrafvb  31933  afvres  31951  mapsnop  32229  lincext2  32354  snlindsntorlem  32369  snelpwrVD  32928  bj-snglss  33826  islshpsm  33994  snatpsubN  34763  polatN  34944  atpsubclN  34958  pclfinclN  34963