Theorem snssi 4339

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

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-sn 4178

This theorem is referenced by:  snssd  4340  difsnid  4341  eldifeldifsn  4342  pwpw0  4344  sssn  4358  ssunsn2  4359  tpssi  4369  pwsnALT  4429  snelpwi  4912  intid  4926  frirr  5091  xpsspw  5233  djussxp  5267  dmressnsn  5438  fconst6g  6094  f1sng  6178  dffv2  6271  fvimacnvi  6331  fvimacnvALT  6336  fsn2  6403  fsnunf  6451  abnexg  6964  suceloni  7013  curry1  7269  curry2  7272  ressuppss  7314  ressuppssdif  7316  mapsn  7899  ralxpmap  7907  fodomr  8111  sucdom2  8156  en1eqsn  8190  enp1ilem  8194  findcard2  8200  findcard2s  8201  marypha1lem  8339  marypha2lem1  8341  epfrs  8607  dfac5lem4  8949  kmlem11  8982  ackbij1lem2  9043  fin23lem26  9147  isfin1-3  9208  hsmexlem4  9251  axdc3lem4  9275  axresscn  9969  nn0ssre  11296  xrsupss  12139  supxrmnf  12147  1exp  12889  hashxrcl  13148  hashdifsn  13202  brfi1indlem  13278  repsdf2  13525  modfsummods  14525  fsum00  14530  incexc  14569  fprodsplit1f  14721  2ebits  15169  bitsinvp1  15171  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  coprmproddvdslem  15376  4sqlem19  15667  ramxrcl  15721  strlemor1OLD  15969  mrcsncl  16272  acsfn1  16322  homaf  16680  dmcoass  16716  lubel  17122  gsumws1  17376  cycsubg2  17631  cntzsnval  17757  0frgp  18192  dpjidcl  18457  ablfac1eu  18472  lspsncl  18977  lspsnss  18990  lspsnid  18993  lpival  19245  lpiss  19250  lidldvgen  19255  znlidl  19881  frlmlbs  20136  mat1dimelbas  20277  smadiadetglem2  20478  isneip  20909  neips  20917  opnneip  20923  maxlp  20951  restsn2  20975  leordtval2  21016  ist1-3  21153  ordtt1  21183  2ndcdisj2  21260  uffix  21725  neiflim  21778  ptcmplem5  21860  cnextfres1  21872  haustsms2  21940  ust0  22023  ustuqtop5  22049  dscopn  22378  icccmplem1  22625  bndth  22757  ovolsn  23263  icombl1  23331  plyun0  23953  coeeulem  23980  coeeu  23981  vieta1lem2  24066  aalioulem2  24088  taylfval  24113  perfectlem2  24955  istrkg2ld  25359  axlowdimlem7  25828  axlowdimlem10  25831  hsn0elch  28105  chsupsn  28272  chsup0  28407  h1deoi  28408  h1dei  28409  h1did  28410  h1de2ctlem  28414  h1de2ci  28415  spansni  28416  spansnch  28419  elspansncl  28424  spansnpji  28437  spanunsni  28438  spanpr  28439  h1datomi  28440  spansnji  28505  h1da  29208  atom1d  29212  superpos  29213  disjun0  29408  esumnul  30110  esumcst  30125  hashf2  30146  esum2d  30155  measvuni  30277  cntnevol  30291  eulerpartlemt  30433  eulerpartlemmf  30437  eulerpartlemgh  30440  ballotlemfp1  30553  reprinfz1  30700  dfon2lem3  31690  noextend  31819  noextendseq  31820  conway  31910  etasslt  31920  altxpsspw  32084  bj-snglss  32958  lindsenlbs  33404  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  mblfinlem2  33447  dvasin  33496  fdc  33541  prnc  33866  isfldidl  33867  ispridlc  33869  islshpsm  34267  snatpsubN  35036  polatN  35217  atpsubclN  35231  pclfinclN  35236  mapfzcons  37279  mzpcompact2lem  37314  diophrw  37322  brfvidRP  37980  cotrcltrcl  38017  corcltrcl  38031  cotrclrcl  38034  gneispa  38428  binomcxplemnotnn0  38555  snelpwrVD  39066  disjiun2  39226  mapsnd  39388  infxrpnf  39674  mccllem  39829  islptre  39851  cncfdmsn  40103  snmbl  40179  stoweidlem44  40261  sge0tsms  40597  sge0iunmptlemfi  40630  ismeannd  40684  isomenndlem  40744  hoidmvlelem3  40811  hoidmvlelem4  40812  ovnhoilem1  40815  fnbrafvb  41234  afvres  41252  perfectALTVlem2  41631  mapsnop  42123  lincext2  42244  snlindsntorlem  42259  aacllem  42547