Theorem snssi 4156

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 4145	. 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 1802   C_ wss 3459   {csn 4011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-v 3095  df-in 3466  df-ss 3473  df-sn 4012

This theorem is referenced by:  difsnid  4158  pwpw0  4160  sssn  4170  ssunsn2  4171  tpssi  4178  pwsnALT  4226  snelpwi  4679  intid  4692  xpsspw  5103  xpsspwOLD  5104  djussxp  5135  dmressnsn  5299  xpimasnOLD  5440  fconst6g  5761  dffv2  5928  fvimacnvi  5983  fvimacnvALT  5988  fsn2  6053  fsnunf  6091  suceloni  6630  curry1  6874  curry2  6877  ressuppss  6918  ressuppssdif  6920  mapsn  7459  ralxpmap  7467  fodomr  7667  sucdom2  7713  en1eqsn  7748  enp1ilem  7753  findcard2  7759  findcard2s  7760  marypha1lem  7892  marypha2lem1  7894  epfrs  8162  dfac5lem4  8507  kmlem11  8540  ackbij1lem2  8601  fin23lem26  8705  isfin1-3  8766  hsmexlem4  8809  axdc3lem4  8833  axresscn  9525  nn0ssre  10802  xrsupss  11506  supxrmnf  11515  1fv  11797  1exp  12171  hashxrcl  12405  hashdifsn  12453  brfi1indlem  12507  snopiswrd  12532  repsdf2  12726  modfsummods  13583  fsum00  13588  incexc  13625  xpnnenOLD  13817  2ebits  13971  bitsinvp1  13973  4sqlem19  14355  ramxrcl  14409  strlemor1  14598  mrcsncl  14883  acsfn1  14932  homaf  15228  dmcoass  15264  lubel  15623  gsumws1  15878  cycsubg2  16109  cntzsnval  16233  0frgp  16668  dpjidcl  16978  dpjidclOLD  16985  ablfac1eu  16995  lspsncl  17494  lspsnss  17507  lspsnid  17510  lpival  17764  lpiss  17769  lidldvgen  17774  znlidl  18440  znlidlOLD  18444  frgpcyg  18482  frlmlbs  18701  mat1dimelbas  18843  mat1dimmul  18848  smadiadetglem2  19044  isneip  19476  neips  19484  opnneip  19490  maxlp  19518  restsn2  19542  leordtval2  19583  ist1-3  19720  ordtt1  19750  2ndcdisj2  19828  uffix  20292  neiflim  20345  ptcmplem5  20426  cnextfres  20438  haustsms2  20505  ust0  20592  ustuqtop5  20618  dscopn  20964  icccmplem1  21197  bndth  21328  ovolsn  21776  icombl1  21843  plyun0  22464  coeeulem  22491  coeeu  22492  vieta1lem2  22576  aalioulem2  22598  taylfval  22623  perfectlem2  23374  istrkg2ld  23727  axlowdimlem7  24120  axlowdimlem10  24123  konigsberg  24856  hsn0elch  26035  chsupsn  26200  chsup0  26335  h1deoi  26336  h1dei  26337  h1did  26338  h1de2ctlem  26342  h1de2ci  26343  spansni  26344  spansnch  26347  elspansncl  26352  spansnpji  26365  spanunsni  26366  spanpr  26367  h1datomi  26368  spansnji  26433  h1da  27137  atom1d  27141  superpos  27142  esumnul  27929  esumcst  27941  hashf2  27960  measvuni  28055  cntnevol  28069  eulerpartlemt  28180  eulerpartlemmf  28184  eulerpartlemgh  28187  ballotlemfp1  28300  dfon2lem3  29189  altxpsspw  29599  mblfinlem2  30024  dvasin  30075  fdc  30210  prnc  30436  isfldidl  30437  ispridlc  30439  mapfzcons  30620  mzpcompact2lem  30656  diophrw  30664  islptre  31533  cncfdmsn  31600  snmbl  31652  stoweidlem44  31715  fnbrafvb  32077  afvres  32095  mapsnop  32662  lincext2  32786  snlindsntorlem  32801  snelpwrVD  33359  bj-snglss  34261  islshpsm  34428  snatpsubN  35197  polatN  35378  atpsubclN  35392  pclfinclN  35397